let A be set ; :: thesis: ( A is finite implies for X being Subset-Family of A st X <> {} holds
ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) ) )
assume A1: A is finite ; :: thesis: for X being Subset-Family of A st X <> {} holds
ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) )
let X be Subset-Family of A; :: thesis: ( X <> {} implies ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) ) )
assume A2: X <> {} ; :: thesis: ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) )
consider p being Function such that
A3: rng p = A and
A4: dom p in omega by A1, Def1;
defpred S₁[ set ] means p .: $1 in X;
consider G being set such that
A5: for x being set holds
( x in G iff ( x in bool (dom p) & S₁[x] ) ) from XBOOLE_0:sch 1();
G c= bool (dom p)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in G or x in bool (dom p) )
assume x in G ; :: thesis: x in bool (dom p)
hence x in bool (dom p) by A5; :: thesis: verum

end;

then reconsider GX = G as Subset-Family of (dom p) ;
consider x being Element of X;
x is Subset of A by A2, TARSKI:def 3;
then A6: p .: (p " x) = x by A3, FUNCT_1:147;
p " x c= dom p by RELAT_1:167;
then A7: GX <> {} by A2, A5, A6;
defpred S₂[ set ] means ( $1 in omega implies for X being Subset-Family of $1 st X <> {} holds
ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) ) );
A8: S₂[ {} ]

proof

assume {} in omega ; :: thesis: for X being Subset-Family of {} st X <> {} holds
ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) )
let X be Subset-Family of {} ; :: thesis: ( X <> {} implies ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) ) )
assume X <> {} ; :: thesis: ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) )
then A9: X = {{} } by ZFMISC_1:1, ZFMISC_1:39;
take {} ; :: thesis: ( {} in X & ( for B being set st B in X & {} c= B holds
B = {} ) )
thus ( {} in X & ( for B being set st B in X & {} c= B holds
B = {} ) ) by A9, TARSKI:def 1; :: thesis: verum

end;

A10: for O being Ordinal st S₂[O] holds
S₂[ succ O]

proof

let O be Ordinal; :: thesis: ( S₂[O] implies S₂[ succ O] )
assume A11: ( O in omega implies for X being Subset-Family of O st X <> {} holds
ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) ) ) ; :: thesis: S₂[ succ O]
thus ( succ O in omega implies for X being Subset-Family of (succ O) st X <> {} holds
ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) ) ) :: thesis: verum

proof

assume succ O in omega ; :: thesis: for X being Subset-Family of (succ O) st X <> {} holds
ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) )
then A12: succ O c= omega by ORDINAL1:def 2;
let X be Subset-Family of (succ O); :: thesis: ( X <> {} implies ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) ) )
assume A13: X <> {} ; :: thesis: ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) )
defpred S₃[ set ] means ex A being set st
( A in X & $1 = A \ {O} );
consider X1 being set such that
A14: for x being set holds
( x in X1 iff ( x in bool O & S₃[x] ) ) from XBOOLE_0:sch 1();
X1 c= bool O

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X1 or x in bool O )
assume x in X1 ; :: thesis: x in bool O
hence x in bool O by A14; :: thesis: verum

end;

then reconsider X2 = X1 as Subset-Family of O ;
consider y being Element of X;
A15: succ O = O \/ {O} by ORDINAL1:def 1;
y is Subset of (succ O) by A13, TARSKI:def 3;
then y \ {O} c= (O \/ {O}) \ {O} by A15, XBOOLE_1:33;
then A16: y \ {O} c= O \ {O} by XBOOLE_1:40;
A17: O in succ O by ORDINAL1:10;
A18: not O in O ;
then y \ {O} c= O by A16, ZFMISC_1:65;
then X2 <> {} by A13, A14;
then consider Z being set such that
A19: ( Z in X2 & ( for B being set st B in X2 & Z c= B holds
B = Z ) ) by A11, A12, A17;
consider X1 being set such that
A20: ( X1 in X & Z = X1 \ {O} ) by A14, A19;
A21: O in {O} by TARSKI:def 1;
then A22: not O in Z by A20, XBOOLE_0:def 5;

A23: now

assume A24: Z \/ {O} in X ; :: thesis: ex A being set ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) )
take A = Z \/ {O}; :: thesis: ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) )
for B being set st B in X & A c= B holds
B = A

proof

let B be set ; :: thesis: ( B in X & A c= B implies B = A )
assume A25: B in X ; :: thesis: ( not A c= B or B = A )
assume A26: A c= B ; :: thesis: B = A

A27: now

assume A28: O in B ; :: thesis: B = A
set Y = B \ {O};
{O} c= B by A28, ZFMISC_1:37;
then A29: B = (B \ {O}) \/ {O} by XBOOLE_1:45;
A \ {O} c= B \ {O} by A26, XBOOLE_1:33;
then ( Z \ {O} c= B \ {O} & not O in Z ) by A20, A21, XBOOLE_0:def 5, XBOOLE_1:40;
then A30: Z c= B \ {O} by ZFMISC_1:65;
B \ {O} c= (O \/ {O}) \ {O} by A15, A25, XBOOLE_1:33;
then B \ {O} c= O \ {O} by XBOOLE_1:40;
then B \ {O} c= O by A18, ZFMISC_1:65;
then B \ {O} in X2 by A14, A25;
hence B = A by A19, A29, A30; :: thesis: verum

end;

now

assume A31: not O in B ; :: thesis: contradiction
O in {O} by TARSKI:def 1;
then O in A by XBOOLE_0:def 3;
hence contradiction by A26, A31; :: thesis: verum

end;

hence B = A by A27; :: thesis: verum

end;

hence ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) ) by A24; :: thesis: verum

end;

now

assume A32: not Z \/ {O} in X ; :: thesis: ex A, x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) )
take A = Z; :: thesis: ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) )

now

assume O in X1 ; :: thesis: contradiction
then X1 = X1 \/ {O} by ZFMISC_1:46
.= Z \/ {O} by A20, XBOOLE_1:39 ;
hence contradiction by A20, A32; :: thesis: verum

end;

then A33: A in X by A20, ZFMISC_1:65;
for B being set st B in X & A c= B holds
B = A

proof

let B be set ; :: thesis: ( B in X & A c= B implies B = A )
assume A34: B in X ; :: thesis: ( not A c= B or B = A )
then B \ {O} c= (O \/ {O}) \ {O} by A15, XBOOLE_1:33;
then B \ {O} c= O \ {O} by XBOOLE_1:40;
then B \ {O} c= O by A18, ZFMISC_1:65;
then A35: B \ {O} in X2 by A14, A34;
assume A36: A c= B ; :: thesis: B = A
then A \ {O} c= B \ {O} by XBOOLE_1:33;
then A37: A c= B \ {O} by A22, ZFMISC_1:65;

A38: now

assume A39: O in B ; :: thesis: contradiction
A \/ {O} = (B \ {O}) \/ {O} by A19, A35, A37
.= B \/ {O} by XBOOLE_1:39
.= B by A39, ZFMISC_1:46 ;
hence contradiction by A32, A34; :: thesis: verum

end;

B c= O

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in O )
assume A40: x in B ; :: thesis: x in O
( x in O or x in {O} ) by A15, A34, A40, XBOOLE_0:def 3;
hence x in O by A38, A40, TARSKI:def 1; :: thesis: verum

end;

then ( B \ {O} = B & B in bool O ) by A38, ZFMISC_1:65;
then B in X2 by A14, A34;
hence B = A by A19, A36; :: thesis: verum

end;

hence ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) ) by A33; :: thesis: verum

end;

hence ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) ) by A23; :: thesis: verum

end;

end;

A41: for O being Ordinal st O <> {} & O is limit_ordinal & ( for B being Ordinal st B in O holds
S₂[B] ) holds
S₂[O]

proof

let O be Ordinal; :: thesis: ( O <> {} & O is limit_ordinal & ( for B being Ordinal st B in O holds
S₂[B] ) implies S₂[O] )
assume that
A42: O <> {} and
A43: O is limit_ordinal and
for B being Ordinal st B in O holds
S₂[B] and
A44: O in omega ; :: thesis: for X being Subset-Family of O st X <> {} holds
ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) )
{} in O by A42, ORDINAL1:24;
then omega c= O by A43, ORDINAL1:def 12;
then O in O by A44;
hence for X being Subset-Family of O st X <> {} holds
ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) ) ; :: thesis: verum

end;

A45: for O being Ordinal holds S₂[O] from ORDINAL2:sch 1(A8, A10, A41);
consider g being set such that
A46: ( g in GX & ( for B being set st B in GX & g c= B holds
B = g ) ) by A4, A7, A45;
take p .: g ; :: thesis: ( p .: g in X & ( for B being set st B in X & p .: g c= B holds
B = p .: g ) )
for B being set st B in X & p .: g c= B holds
B = p .: g

proof

let B be set ; :: thesis: ( B in X & p .: g c= B implies B = p .: g )
assume A47: B in X ; :: thesis: ( not p .: g c= B or B = p .: g )
assume p .: g c= B ; :: thesis: B = p .: g
then A48: p " (p .: g) c= p " B by RELAT_1:178;
A49: g c= p " (p .: g) by A46, FUNCT_1:146;
A50: p .: (p " B) = B by A3, A47, FUNCT_1:147;
p " B c= dom p by RELAT_1:167;
then p " B in GX by A5, A47, A50;
hence B = p .: g by A46, A48, A49, A50, XBOOLE_1:1; :: thesis: verum

end;

hence ( p .: g in X & ( for B being set st B in X & p .: g c= B holds
B = p .: g ) ) by A5, A46; :: thesis: verum