let T be 1-sorted ; :: thesis: for F being finite Subset-Family of T
for F1 being Subset-Family of T st F is Cover of T & F1 = F \ { X where X is Subset of T : ( X in F & ex Y being Subset of T st
( Y in F & X c< Y ) ) } holds
F1 is Cover of T
let F be finite Subset-Family of T; :: thesis: for F1 being Subset-Family of T st F is Cover of T & F1 = F \ { X where X is Subset of T : ( X in F & ex Y being Subset of T st
( Y in F & X c< Y ) ) } holds
F1 is Cover of T
let F1 be Subset-Family of T; :: thesis: ( F is Cover of T & F1 = F \ { X where X is Subset of T : ( X in F & ex Y being Subset of T st
( Y in F & X c< Y ) ) } implies F1 is Cover of T )
assume that
A1: the carrier of T c= union F and
A2: F1 = F \ { X where X is Subset of T : ( X in F & ex Y being Subset of T st
( Y in F & X c< Y ) ) } ; :: according to SETFAM_1:def 11 :: thesis: F1 is Cover of T
set ZAW = { X where X is Subset of T : ( X in F & ex Y being Subset of T st
( Y in F & X c< Y ) ) } ;
thus the carrier of T c= union F1 :: according to SETFAM_1:def 11 :: thesis: verum
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in the carrier of T or t in union F1 )
assume t in the carrier of T ; :: thesis: t in union F1
then consider Z being set such that
A3: t in Z and
A4: Z in F by A1, TARSKI:def 4;
set ALL = { X where X is Subset of T : ( Z c< X & X in F ) } ;
per cases ( { X where X is Subset of T : ( Z c< X & X in F ) } is empty or not { X where X is Subset of T : ( Z c< X & X in F ) } is empty ) ;
suppose A5: { X where X is Subset of T : ( Z c< X & X in F ) } is empty ; :: thesis: t in union F1
now :: thesis: not Z in { X where X is Subset of T : ( X in F & ex Y being Subset of T st
( Y in F & X c< Y ) ) }
assume Z in { X where X is Subset of T : ( X in F & ex Y being Subset of T st
( Y in F & X c< Y ) ) } ; :: thesis: contradiction
then consider X being Subset of T such that
A6: Z = X and
X in F and
A7: ex Y being Subset of T st
( Y in F & X c< Y ) ;
consider Y being Subset of T such that
A8: ( Y in F & X c< Y ) by A7;
Y in { X where X is Subset of T : ( Z c< X & X in F ) } by A6, A8;
hence contradiction by A5; :: thesis: verum
end;
then Z in F1 by A2, A4, XBOOLE_0:def 5;
hence t in union F1 by A3, TARSKI:def 4; :: thesis: verum
end;
suppose not { X where X is Subset of T : ( Z c< X & X in F ) } is empty ; :: thesis: t in union F1
then consider w being object such that
A9: w in { X where X is Subset of T : ( Z c< X & X in F ) } ;
consider R being Relation of { X where X is Subset of T : ( Z c< X & X in F ) } such that
A10: for x, y being set holds
( [x,y] in R iff ( x in { X where X is Subset of T : ( Z c< X & X in F ) } & y in { X where X is Subset of T : ( Z c< X & X in F ) } & S1[x,y] ) ) from RELSET_1:sch 5();
A11: R is_reflexive_in { X where X is Subset of T : ( Z c< X & X in F ) } by A10;
then A12: field R = { X where X is Subset of T : ( Z c< X & X in F ) } by ORDERS_1:13;
A13: R partially_orders { X where X is Subset of T : ( Z c< X & X in F ) }
proof
thus R is_reflexive_in { X where X is Subset of T : ( Z c< X & X in F ) } by A11; :: according to ORDERS_1:def 8 :: thesis: ( R is_transitive_in { X where X is Subset of T : ( Z c< X & X in F ) } & R is_antisymmetric_in { X where X is Subset of T : ( Z c< X & X in F ) } )
thus R is_transitive_in { X where X is Subset of T : ( Z c< X & X in F ) } :: thesis: R is_antisymmetric_in { X where X is Subset of T : ( Z c< X & X in F ) }
proof
let x, y, z be object ; :: according to RELAT_2:def 8 :: thesis: ( not x in { X where X is Subset of T : ( Z c< X & X in F ) } or not y in { X where X is Subset of T : ( Z c< X & X in F ) } or not z in { X where X is Subset of T : ( Z c< X & X in F ) } or not [x,y] in R or not [y,z] in R or [x,z] in R )
assume that
A14: x in { X where X is Subset of T : ( Z c< X & X in F ) } and
y in { X where X is Subset of T : ( Z c< X & X in F ) } and
A15: z in { X where X is Subset of T : ( Z c< X & X in F ) } ; :: thesis: ( not [x,y] in R or not [y,z] in R or [x,z] in R )
assume A16: ( [x,y] in R & [y,z] in R ) ; :: thesis: [x,z] in R
reconsider x = x, y = y, z = z as set by TARSKI:1;
( x c= y & y c= z ) by A10, A16;
then x c= z ;
hence [x,z] in R by A10, A14, A15; :: thesis: verum
end;
let x, y be object ; :: according to RELAT_2:def 4 :: thesis: ( not x in { X where X is Subset of T : ( Z c< X & X in F ) } or not y in { X where X is Subset of T : ( Z c< X & X in F ) } or not [x,y] in R or not [y,x] in R or x = y )
assume that
x in { X where X is Subset of T : ( Z c< X & X in F ) } and
y in { X where X is Subset of T : ( Z c< X & X in F ) } ; :: thesis: ( not [x,y] in R or not [y,x] in R or x = y )
assume A17: ( [x,y] in R & [y,x] in R ) ; :: thesis: x = y
reconsider x = x, y = y as set by TARSKI:1;
( x c= y & y c= x ) by A10, A17;
hence x = y by XBOOLE_0:def 10; :: thesis: verum
end;
A18: R is reflexive by A11, A12;
{ X where X is Subset of T : ( Z c< X & X in F ) } has_upper_Zorn_property_wrt R
proof
let Y be set ; :: according to ORDERS_1:def 10 :: thesis: ( not Y c= { X where X is Subset of T : ( Z c< X & X in F ) } or not R |_2 Y is being_linear-order or ex b1 being set st
( b1 in { X where X is Subset of T : ( Z c< X & X in F ) } & ( for b2 being set holds
( not b2 in Y or [b2,b1] in R ) ) ) )
assume that
A19: Y c= { X where X is Subset of T : ( Z c< X & X in F ) } and
A20: R |_2 Y is being_linear-order ; :: thesis: ex b1 being set st
( b1 in { X where X is Subset of T : ( Z c< X & X in F ) } & ( for b2 being set holds
( not b2 in Y or [b2,b1] in R ) ) )
per cases ( not Y is empty or Y is empty ) ;
suppose A21: not Y is empty ; :: thesis: ex b1 being set st
( b1 in { X where X is Subset of T : ( Z c< X & X in F ) } & ( for b2 being set holds
( not b2 in Y or [b2,b1] in R ) ) )
defpred S2[ set ] means ( not $1 is empty & $1 c= Y implies union $1 in Y );
take union Y ; :: thesis: ( union Y in { X where X is Subset of T : ( Z c< X & X in F ) } & ( for b1 being set holds
( not b1 in Y or [b1,(union Y)] in R ) ) )
A22: S2[ {} ] ;
A23: for A, B being set st A in Y & B in Y holds
A \/ B in Y
proof
A24: R |_2 Y c= R by XBOOLE_1:17;
R |_2 Y is connected by A20;
then A25: R |_2 Y is_connected_in field (R |_2 Y) ;
let A, B be set ; :: thesis: ( A in Y & B in Y implies A \/ B in Y )
assume A26: ( A in Y & B in Y ) ; :: thesis: A \/ B in Y
field (R |_2 Y) = Y by A12, A18, A19, ORDERS_1:71;
then ( [A,B] in R |_2 Y or [B,A] in R |_2 Y or A = B ) by A26, A25;
then ( A c= B or B c= A ) by A10, A24;
hence A \/ B in Y by A26, XBOOLE_1:12; :: thesis: verum
end;
A27: for x, B being set st x in Y & B c= Y & S2[B] holds
S2[B \/ {x}]
proof
let x, B be set ; :: thesis: ( x in Y & B c= Y & S2[B] implies S2[B \/ {x}] )
assume that
A28: x in Y and
A29: ( B c= Y & S2[B] ) and
not B \/ {x} is empty and
B \/ {x} c= Y ; :: thesis: union (B \/ {x}) in Y
A30: union {x} = x by ZFMISC_1:25;
end;
consider y being object such that
A31: y in Y by A21;
y in { X where X is Subset of T : ( Z c< X & X in F ) } by A19, A31;
then consider X being Subset of T such that
A32: X = y and
A33: Z c< X and
X in F ;
A34: X c= union Y by A31, A32, ZFMISC_1:74;
then A35: Z <> union Y by A33, XBOOLE_0:def 8;
Z c= X by A33;
then Z c= union Y by A34;
then A36: Z c< union Y by A35;
A37: { X where X is Subset of T : ( Z c< X & X in F ) } c= F
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { X where X is Subset of T : ( Z c< X & X in F ) } or x in F )
assume x in { X where X is Subset of T : ( Z c< X & X in F ) } ; :: thesis: x in F
then ex X being Subset of T st
( X = x & Z c< X & X in F ) ;
hence x in F ; :: thesis: verum
end;
then A38: Y c= F by A19;
A39: Y is finite by A19, A37;
S2[Y] from FINSET_1:sch 2(A39, A22, A27);
then union Y in F by A21, A38;
hence A40: union Y in { X where X is Subset of T : ( Z c< X & X in F ) } by A36; :: thesis: for b1 being set holds
( not b1 in Y or [b1,(union Y)] in R )
let z be set ; :: thesis: ( not z in Y or [z,(union Y)] in R )
assume A41: z in Y ; :: thesis: [z,(union Y)] in R
then S1[z, union Y] by ZFMISC_1:74;
hence [z,(union Y)] in R by A10, A19, A40, A41; :: thesis: verum
end;
suppose A42: Y is empty ; :: thesis: ex b1 being set st
( b1 in { X where X is Subset of T : ( Z c< X & X in F ) } & ( for b2 being set holds
( not b2 in Y or [b2,b1] in R ) ) )
reconsider w = w as set by TARSKI:1;
take w ; :: thesis: ( w in { X where X is Subset of T : ( Z c< X & X in F ) } & ( for b1 being set holds
( not b1 in Y or [b1,w] in R ) ) )
thus w in { X where X is Subset of T : ( Z c< X & X in F ) } by A9; :: thesis: for b1 being set holds
( not b1 in Y or [b1,w] in R )
thus for b1 being set holds
( not b1 in Y or [b1,w] in R ) by A42; :: thesis: verum
end;
end;
end;
then consider M being set such that
A43: M is_maximal_in R by A12, A13, ORDERS_1:63;
A44: M in field R by A43;
then A45: ex X being Subset of T st
( X = M & Z c< X & X in F ) by A12;
now :: thesis: not M in { X where X is Subset of T : ( X in F & ex Y being Subset of T st
( Y in F & X c< Y ) ) }
assume M in { X where X is Subset of T : ( X in F & ex Y being Subset of T st
( Y in F & X c< Y ) ) } ; :: thesis: contradiction
then consider H being Subset of T such that
A46: M = H and
H in F and
A47: ex Y being Subset of T st
( Y in F & H c< Y ) ;
consider Y being Subset of T such that
A48: Y in F and
A49: H c< Y by A47;
Z c< Y by A45, A46, A49, XBOOLE_1:56;
then A50: Y in { X where X is Subset of T : ( Z c< X & X in F ) } by A48;
H c= Y by A49;
then [M,Y] in R by A10, A12, A44, A46, A50;
hence contradiction by A12, A43, A46, A49, A50; :: thesis: verum
end;
then A51: M in F1 by A2, A45, XBOOLE_0:def 5;
Z c= M by A45;
hence t in union F1 by A3, A51, TARSKI:def 4; :: thesis: verum
end;
end;
end;