let X be finite set ; :: thesis: for M, F being Dependency-set of X st M is (M1) & M is (M2) & M is (M3) & F = { [A,B] where A, B is Subset of : ex A', B' being Subset of st
( [A',B'] >= [A,B] & [A',B'] in M ) } holds
( M = Maximal_wrt F & F is full_family & ( for G being Full-family of X st M = Maximal_wrt G holds
G = F ) )
let M, F be Dependency-set of X; :: thesis: ( M is (M1) & M is (M2) & M is (M3) & F = { [A,B] where A, B is Subset of : ex A', B' being Subset of st
( [A',B'] >= [A,B] & [A',B'] in M ) } implies ( M = Maximal_wrt F & F is full_family & ( for G being Full-family of X st M = Maximal_wrt G holds
G = F ) ) )
assume that
A1: ( M is (M1) & M is (M2) & M is (M3) ) and
A2: F = { [A,B] where A, B is Subset of : ex A', B' being Subset of st
( [A',B'] >= [A,B] & [A',B'] in M ) } ; :: thesis: ( M = Maximal_wrt F & F is full_family & ( for G being Full-family of X st M = Maximal_wrt G holds
G = F ) )
A3: F is (F1)
proof
let A be Subset of ; :: according to ARMSTRNG:def 12 :: thesis: [A,A] in F
ex A', B' being Subset of st
( [A',B'] >= [A,A] & [A',B'] in M ) by A1, Def19;
hence [A,A] in F by A2; :: thesis: verum
end;
A4: now
let x be set ; :: thesis: ( x in F implies ex a, b, a', b' being Subset of st
( x = [a,b] & [a',b'] >= [a,b] & [a',b'] in M ) )
assume x in F ; :: thesis: ex a, b, a', b' being Subset of st
( x = [a,b] & [a',b'] >= [a,b] & [a',b'] in M )
then consider a, b being Subset of such that
A5: x = [a,b] and
A6: ex a', b' being Subset of st
( [a',b'] >= [a,b] & [a',b'] in M ) by A2;
consider a', b' being Subset of such that
A7: [a',b'] >= [a,b] and
A8: [a',b'] in M by A6;
take a = a; :: thesis: ex b, a', b' being Subset of st
( x = [a,b] & [a',b'] >= [a,b] & [a',b'] in M )
take b = b; :: thesis: ex a', b' being Subset of st
( x = [a,b] & [a',b'] >= [a,b] & [a',b'] in M )
take a' = a'; :: thesis: ex b' being Subset of st
( x = [a,b] & [a',b'] >= [a,b] & [a',b'] in M )
take b' = b'; :: thesis: ( x = [a,b] & [a',b'] >= [a,b] & [a',b'] in M )
thus ( x = [a,b] & [a',b'] >= [a,b] & [a',b'] in M ) by A5, A7, A8; :: thesis: verum
end;
A9: now
let A, B be Subset of ; :: thesis: ( [A,B] in F implies ex a', b' being Subset of st
( [a',b'] >= [A,B] & [a',b'] in M ) )
assume [A,B] in F ; :: thesis: ex a', b' being Subset of st
( [a',b'] >= [A,B] & [a',b'] in M )
then consider a, b, a', b' being Subset of such that
A10: [A,B] = [a,b] and
A11: [a',b'] >= [a,b] and
A12: [a',b'] in M by A4;
take a' = a'; :: thesis: ex b' being Subset of st
( [a',b'] >= [A,B] & [a',b'] in M )
take b' = b'; :: thesis: ( [a',b'] >= [A,B] & [a',b'] in M )
thus ( [a',b'] >= [A,B] & [a',b'] in M ) by A10, A11, A12; :: thesis: verum
end;
now
let A, B, C be Subset of ; :: thesis: ( [A,B] in F & [B,C] in F implies [A,C] in F )
assume that
A13: [A,B] in F and
A14: [B,C] in F ; :: thesis: [A,C] in F
consider A', B' being Subset of such that
A15: [A',B'] >= [A,B] and
A16: [A',B'] in M by A9, A13;
consider B1', C' being Subset of such that
A17: [B1',C'] >= [B,C] and
A18: [B1',C'] in M by A9, A14;
A19: B1' c= B by A17, Th15;
B c= B' by A15, Th15;
then B1' c= B' by A19, XBOOLE_1:1;
then C' c= B' by A1, A16, A18, Def21;
then A20: [A',B'] >= [A',C'] by Th15;
A21: C c= C' by A17, Th15;
A' c= A by A15, Th15;
then [A',C'] >= [A,C] by A21, Th15;
then [A',B'] >= [A,C] by A20, Th14;
hence [A,C] in F by A2, A16; :: thesis: verum
end;
then A22: F is (F2) by Th20;
A23: F is (F4)
proof
let A, B, A', B' be Subset of ; :: according to ARMSTRNG:def 14 :: thesis: ( [A,B] in F & [A',B'] in F implies [(A \/ A'),(B \/ B')] in F )
assume that
A24: [A,B] in F and
A25: [A',B'] in F ; :: thesis: [(A \/ A'),(B \/ B')] in F
consider a1, b1 being Subset of such that
A26: [a1,b1] >= [A,B] and
A27: [a1,b1] in M by A9, A24;
A28: B c= b1 by A26, Th15;
consider a1', b1' being Subset of such that
A29: [a1',b1'] >= [A',B'] and
A30: [a1',b1'] in M by A9, A25;
A31: B' c= b1' by A29, Th15;
consider A'', B'' being Subset of such that
A32: [A'',B''] >= [(A \/ A'),(A \/ A')] and
A33: [A'',B''] in M by A1, Def19;
A34: A \/ A' c= B'' by A32, Th15;
a1' c= A' by A29, Th15;
then a1' c= A \/ A' by XBOOLE_1:10;
then a1' c= B'' by A34, XBOOLE_1:1;
then b1' c= B'' by A1, A33, A30, Def21;
then A35: B' c= B'' by A31, XBOOLE_1:1;
a1 c= A by A26, Th15;
then a1 c= A \/ A' by XBOOLE_1:10;
then a1 c= B'' by A34, XBOOLE_1:1;
then b1 c= B'' by A1, A33, A27, Def21;
then B c= B'' by A28, XBOOLE_1:1;
then A36: B \/ B' c= B'' \/ B'' by A35, XBOOLE_1:13;
A'' c= A \/ A' by A32, Th15;
then [A'',B''] >= [(A \/ A'),(B \/ B')] by A36, Th15;
hence [(A \/ A'),(B \/ B')] in F by A2, A33; :: thesis: verum
end;
set DOX = Dependencies-Order X;
now
let x be set ; :: thesis: ( ( x in M implies x in Maximal_wrt F ) & ( x in Maximal_wrt F implies x in M ) )
hereby :: thesis: ( x in Maximal_wrt F implies x in M )
assume A37: x in M ; :: thesis: x in Maximal_wrt F
then consider a, b being Subset of such that
A38: x = [a,b] by Th10;
x is_maximal_wrt F, Dependencies-Order X
proof
thus x in F by A2, A37, A38; :: according to WAYBEL_4:def 24 :: thesis: for b1 being set holds
( not b1 in F or b1 = x or not [x,b1] in Dependencies-Order X )
given y being set such that A39: y in F and
A40: y <> x and
A41: [x,y] in Dependencies-Order X ; :: thesis: contradiction
consider e, f being Dependency of X such that
A42: [x,y] = [e,f] and
A43: e <= f by A41;
A44: y = f by A42, ZFMISC_1:33;
consider c, d, c', d' being Subset of such that
A45: y = [c,d] and
A46: [c',d'] >= [c,d] and
A47: [c',d'] in M by A4, A39;
A48: x = e by A42, ZFMISC_1:33;
then A49: [c',d'] >= [a,b] by A38, A43, A44, A45, A46, Th14;
then A50: d' = b by A1, A37, A38, A47, Def20;
c' = a by A1, A37, A38, A47, A49, Def20;
hence contradiction by A38, A40, A43, A48, A44, A45, A46, A50, Th13; :: thesis: verum
end;
hence x in Maximal_wrt F by Def1; :: thesis: verum
end;
assume A51: x in Maximal_wrt F ; :: thesis: x in M
then A52: x is_maximal_wrt F, Dependencies-Order X by Def1;
assume A53: not x in M ; :: thesis: contradiction
consider a, b, a', b' being Subset of such that
A54: x = [a,b] and
A55: [a',b'] >= [a,b] and
A56: [a',b'] in M by A4, A51;
A57: [[a,b],[a',b']] in Dependencies-Order X by A55;
[a',b'] in F by A2, A56;
hence contradiction by A52, A54, A56, A53, A57, WAYBEL_4:def 24; :: thesis: verum
end;
hence M = Maximal_wrt F by TARSKI:2; :: thesis: ( F is full_family & ( for G being Full-family of X st M = Maximal_wrt G holds
G = F ) )
F is (F3)
proof
let A, B, A', B' be Subset of ; :: according to ARMSTRNG:def 13 :: thesis: ( [A,B] in F & [A,B] >= [A',B'] implies [A',B'] in F )
assume that
A58: [A,B] in F and
A59: [A,B] >= [A',B'] ; :: thesis: [A',B'] in F
consider a', b' being Subset of such that
A60: [a',b'] >= [A,B] and
A61: [a',b'] in M by A9, A58;
[a',b'] >= [A',B'] by A59, A60, Th14;
hence [A',B'] in F by A2, A61; :: thesis: verum
end;
hence F is full_family by A3, A22, A23; :: thesis: for G being Full-family of X st M = Maximal_wrt G holds
G = F
let G be Full-family of X; :: thesis: ( M = Maximal_wrt G implies G = F )
assume A62: M = Maximal_wrt G ; :: thesis: G = F
now
let x be set ; :: thesis: ( ( x in G implies x in F ) & ( x in F implies x in G ) )
hereby :: thesis: ( x in F implies x in G )
A63: field (Dependencies-Order X) = [:(bool X),(bool X):] by Th19;
assume A64: x in G ; :: thesis: x in F
then consider a, b being Subset of such that
A65: x = [a,b] by Th10;
defpred S1[ set ] means ex y being Dependency of X st
( $1 = y & y >= [a,b] );
consider MA being set such that
A66: for x being set holds
( x in MA iff ( x in G & S1[x] ) ) from XBOOLE_0:sch 1();
 MA c= G
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in MA or x in G )
assume x in MA ; :: thesis: x in G
hence x in G by A66; :: thesis: verum
end;
then A67: MA is finite Subset of by A63, XBOOLE_1:1;
MA <> {} by A64, A65, A66;
then consider m being Element of MA such that
A68: m is_maximal_wrt MA, Dependencies-Order X by A67, Th2;
A69: m in MA by A68, WAYBEL_4:def 24;
then m in G by A66;
then A70: ex a', b' being Subset of st m = [a',b'] by Th10;
m is_maximal_wrt G, Dependencies-Order X
proof
A71: ex mm being Dependency of X st
( m = mm & mm >= [a,b] ) by A66, A69;
thus m in G by A66, A69; :: according to WAYBEL_4:def 24 :: thesis: for b1 being set holds
( not b1 in G or b1 = m or not [m,b1] in Dependencies-Order X )
given y being set such that A72: y in G and
A73: y <> m and
A74: [m,y] in Dependencies-Order X ; :: thesis: contradiction
consider e, f being Dependency of X such that
A75: [m,y] = [e,f] and
A76: e <= f by A74;
A77: y = f by A75, ZFMISC_1:33;
m = e by A75, ZFMISC_1:33;
then f >= [a,b] by A71, A76, Th14;
then y in MA by A66, A72, A77;
hence contradiction by A68, A73, A74, WAYBEL_4:def 24; :: thesis: verum
end;
then A78: m in (Dependencies-Order X) Maximal_in G by Def1;
ex y being Dependency of X st
( m = y & y >= [a,b] ) by A66, A69;
hence x in F by A2, A62, A65, A78, A70; :: thesis: verum
end;
assume x in F ; :: thesis: x in G
then ex a, b, a1, b1 being Subset of st
( x = [a,b] & [a1,b1] >= [a,b] & [a1,b1] in M ) by A4;
hence x in G by A62, Def13; :: thesis: verum
end;
hence G = F by TARSKI:2; :: thesis: verum