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