let X be non empty finite set ; :: thesis: for G being Subset-Family of X holds G is_generator-set_of saturated-subsets (X deps_encl_by G)
let G be Subset-Family of X; :: thesis: G is_generator-set_of saturated-subsets (X deps_encl_by G)
set F = X deps_encl_by G;
set ssF = saturated-subsets (X deps_encl_by G);
X deps_encl_by G is full_family by Th33;
then A1: ( saturated-subsets (X deps_encl_by G) is (B1) & saturated-subsets (X deps_encl_by G) is (B2) ) by Th32;
thus G is_generator-set_of saturated-subsets (X deps_encl_by G) :: thesis: verum
proof
set H = { (Intersect S) where S is Subset-Family of X : S c= G } ;
thus A2: G c= saturated-subsets (X deps_encl_by G) by Th34; :: according to ARMSTRNG:def 25 :: thesis: saturated-subsets (X deps_encl_by G) = { (Intersect S) where S is Subset-Family of X : S c= G }
now :: thesis: for x being object holds
( ( x in saturated-subsets (X deps_encl_by G) implies x in { (Intersect S) where S is Subset-Family of X : S c= G } ) & ( x in { (Intersect S) where S is Subset-Family of X : S c= G } implies x in saturated-subsets (X deps_encl_by G) ) )
let x be object ; :: thesis: ( ( x in saturated-subsets (X deps_encl_by G) implies x in { (Intersect S) where S is Subset-Family of X : S c= G } ) & ( x in { (Intersect S) where S is Subset-Family of X : S c= G } implies x in saturated-subsets (X deps_encl_by G) ) )
hereby :: thesis: ( x in { (Intersect S) where S is Subset-Family of X : S c= G } implies x in saturated-subsets (X deps_encl_by G) )
assume x in saturated-subsets (X deps_encl_by G) ; :: thesis: x in { (Intersect S) where S is Subset-Family of X : S c= G }
then consider b9, a9 being Subset of X such that
A3: x = b9 and
A4: a9 ^|^ b9,X deps_encl_by G by Th31;
[a9,b9] in Maximal_wrt (X deps_encl_by G) by A4;
then [a9,b9] in X deps_encl_by G ;
then consider a, b being Subset of X such that
A5: [a,b] = [a9,b9] and
A6: for c being set st c in G & a c= c holds
b c= c ;
set C = { c where c is Subset of X : ( c in G & a c= c ) } ;
{ c where c is Subset of X : ( c in G & a c= c ) } c= bool X
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { c where c is Subset of X : ( c in G & a c= c ) } or x in bool X )
assume x in { c where c is Subset of X : ( c in G & a c= c ) } ; :: thesis: x in bool X
then ex c being Subset of X st
( x = c & c in G & a c= c ) ;
hence x in bool X ; :: thesis: verum
end;
then reconsider C = { c where c is Subset of X : ( c in G & a c= c ) } as Subset-Family of X ;
now :: thesis: for z1 being set st z1 in C holds
b c= z1
let z1 be set ; :: thesis: ( z1 in C implies b c= z1 )
assume z1 in C ; :: thesis: b c= z1
then ex c being Subset of X st
( z1 = c & c in G & a c= c ) ;
hence b c= z1 by A6; :: thesis: verum
end;
then A7: b c= Intersect C by MSSUBFAM:4;
set ic = Intersect C;
A8: b = b9 by A5, XTUPLE_0:1;
A9: C c= G
proof
let c be object ; :: according to TARSKI:def 3 :: thesis: ( not c in C or c in G )
assume c in C ; :: thesis: c in G
then ex cc being Subset of X st
( cc = c & cc in G & a c= cc ) ;
hence c in G ; :: thesis: verum
end;
thus x in { (Intersect S) where S is Subset-Family of X : S c= G } :: thesis: verum
proof
per cases ( b = Intersect C or b <> Intersect C ) ;
suppose b = Intersect C ; :: thesis: x in { (Intersect S) where S is Subset-Family of X : S c= G }
hence x in { (Intersect S) where S is Subset-Family of X : S c= G } by A3, A8, A9; :: thesis: verum
end;
suppose A10: b <> Intersect C ; :: thesis: x in { (Intersect S) where S is Subset-Family of X : S c= G }
reconsider ic = Intersect C as Subset of X ;
now :: thesis: for c being set st c in G & a c= c holds
ic c= c
let c be set ; :: thesis: ( c in G & a c= c implies ic c= c )
assume that
A11: c in G and
A12: a c= c ; :: thesis: ic c= c
c in C by A11, A12;
hence ic c= c by MSSUBFAM:2; :: thesis: verum
end;
then A13: [a,ic] in X deps_encl_by G ;
[a,b] <= [a,ic] by A7;
hence x in { (Intersect S) where S is Subset-Family of X : S c= G } by A4, A5, A8, A10, A13, Th27; :: thesis: verum
end;
end;
end;
end;
assume x in { (Intersect S) where S is Subset-Family of X : S c= G } ; :: thesis: x in saturated-subsets (X deps_encl_by G)
then A14: ex S being Subset-Family of X st
( Intersect S = x & S c= G ) ;
thus x in saturated-subsets (X deps_encl_by G) by A1, A2, A14, Th1, XBOOLE_1:1; :: thesis: verum
end;
hence saturated-subsets (X deps_encl_by G) = { (Intersect S) where S is Subset-Family of X : S c= G } by TARSKI:2; :: thesis: verum
end;