:: ZFREFLE1 semantic presentation

begin

Lm1:  {} in omega
by ORDINAL1:def_11;

Lm2:  omega is limit_ordinal
by ORDINAL1:def_11;


definition
let M be non empty set ;
let F be Subset of WFF;
predM |= F means :Def1: :: ZFREFLE1:def 1
 for H being ZF-formula st H in F holds
M |= H;
end;

:: deftheorem Def1 defines |= ZFREFLE1:def_1_:_
 for M being non empty set
for F being Subset of WFF holds
( M |= F iff for H being ZF-formula st H in F holds
M |= H );

definition
let M1, M2 be non empty set ;
predM1 <==> M2 means :: ZFREFLE1:def 2
 for H being ZF-formula st Free H = {} holds
( M1 |= H iff M2 |= H );
reflexivity
 for M1 being non empty set
for H being ZF-formula st Free H = {} holds
( M1 |= H iff M1 |= H ) ;
symmetry
 for M1, M2 being non empty set st ( for H being ZF-formula st Free H = {} holds
( M1 |= H iff M2 |= H ) ) holds
for H being ZF-formula st Free H = {} holds
( M2 |= H iff M1 |= H ) ;
predM1 is_elementary_subsystem_of M2 means :: ZFREFLE1:def 3
( M1 c= M2 & ( for H being ZF-formula
for v being Function of VAR,M1 holds
( M1,v |= H iff M2,M2 ! v |= H ) ) );
reflexivity
 for M1 being non empty set holds
( M1 c= M1 & ( for H being ZF-formula
for v being Function of VAR,M1 holds
( M1,v |= H iff M1,M1 ! v |= H ) ) ) by ZF_LANG1:def_1;
end;

:: deftheorem  defines <==> ZFREFLE1:def_2_:_
 for M1, M2 being non empty set holds
( M1 <==> M2 iff for H being ZF-formula st Free H = {} holds
( M1 |= H iff M2 |= H ) );

:: deftheorem  defines is_elementary_subsystem_of ZFREFLE1:def_3_:_
 for M1, M2 being non empty set holds
( M1 is_elementary_subsystem_of M2 iff ( M1 c= M2 & ( for H being ZF-formula
for v being Function of VAR,M1 holds
( M1,v |= H iff M2,M2 ! v |= H ) ) ) );

defpred S1[ set ] means ( $1 = the_axiom_of_extensionality or $1 = the_axiom_of_pairs or $1 = the_axiom_of_unions or $1 = the_axiom_of_infinity or $1 = the_axiom_of_power_sets or ex H being ZF-formula st
( {(x. 0),(x. 1),(x. 2)} misses Free H & $1 = the_axiom_of_substitution_for H ) );

definition
func ZF-axioms  ->  set  means :Def4: :: ZFREFLE1:def 4
 for e being set holds
( e in it iff ( e in WFF & ( e = the_axiom_of_extensionality or e = the_axiom_of_pairs or e = the_axiom_of_unions or e = the_axiom_of_infinity or e = the_axiom_of_power_sets or ex H being ZF-formula st
( {(x. 0),(x. 1),(x. 2)} misses Free H & e = the_axiom_of_substitution_for H ) ) ) );
existence
 ex b1 being set st
for e being set holds
( e in b1 iff ( e in WFF & ( e = the_axiom_of_extensionality or e = the_axiom_of_pairs or e = the_axiom_of_unions or e = the_axiom_of_infinity or e = the_axiom_of_power_sets or ex H being ZF-formula st
( {(x. 0),(x. 1),(x. 2)} misses Free H & e = the_axiom_of_substitution_for H ) ) ) )
proof
thus  ex X being set st
for e being set holds
( e in X iff ( e in WFF & S1[e] ) ) from XBOOLE_0:sch_1(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for e being set holds
( e in b1 iff ( e in WFF & ( e = the_axiom_of_extensionality or e = the_axiom_of_pairs or e = the_axiom_of_unions or e = the_axiom_of_infinity or e = the_axiom_of_power_sets or ex H being ZF-formula st
( {(x. 0),(x. 1),(x. 2)} misses Free H & e = the_axiom_of_substitution_for H ) ) ) ) ) & ( for e being set holds
( e in b2 iff ( e in WFF & ( e = the_axiom_of_extensionality or e = the_axiom_of_pairs or e = the_axiom_of_unions or e = the_axiom_of_infinity or e = the_axiom_of_power_sets or ex H being ZF-formula st
( {(x. 0),(x. 1),(x. 2)} misses Free H & e = the_axiom_of_substitution_for H ) ) ) ) ) holds
b1 = b2
proof
defpred S2[ set ] means ( $1 in WFF & S1[$1] );
let X1, X2 be set ; ::_thesis: ( ( for e being set holds
( e in X1 iff ( e in WFF & ( e = the_axiom_of_extensionality or e = the_axiom_of_pairs or e = the_axiom_of_unions or e = the_axiom_of_infinity or e = the_axiom_of_power_sets or ex H being ZF-formula st
( {(x. 0),(x. 1),(x. 2)} misses Free H & e = the_axiom_of_substitution_for H ) ) ) ) ) & ( for e being set holds
( e in X2 iff ( e in WFF & ( e = the_axiom_of_extensionality or e = the_axiom_of_pairs or e = the_axiom_of_unions or e = the_axiom_of_infinity or e = the_axiom_of_power_sets or ex H being ZF-formula st
( {(x. 0),(x. 1),(x. 2)} misses Free H & e = the_axiom_of_substitution_for H ) ) ) ) ) implies X1 = X2 )
assume that
A1: for e being set holds
( e in X1 iff S2[e] ) and
A2: for e being set holds
( e in X2 iff S2[e] ) ; ::_thesis: X1 = X2
thus  X1 = X2 from XBOOLE_0:sch_2(A1, A2); ::_thesis: verum
end;
end;

:: deftheorem Def4 defines ZF-axioms ZFREFLE1:def_4_:_
 for b1 being set holds
( b1 = ZF-axioms iff for e being set holds
( e in b1 iff ( e in WFF & ( e = the_axiom_of_extensionality or e = the_axiom_of_pairs or e = the_axiom_of_unions or e = the_axiom_of_infinity or e = the_axiom_of_power_sets or ex H being ZF-formula st
( {(x. 0),(x. 1),(x. 2)} misses Free H & e = the_axiom_of_substitution_for H ) ) ) ) );

definition
:: original: ZF-axioms
redefine func ZF-axioms  ->  Subset of WFF;
coherence
 ZF-axioms is Subset of WFF
proof
 ZF-axioms c= WFF
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in ZF-axioms or e in WFF )
thus  ( not e in ZF-axioms or e in WFF ) by Def4; ::_thesis: verum
end;
hence  ZF-axioms is Subset of WFF ; ::_thesis: verum
end;
end;


theorem :: ZFREFLE1:1
for M being non empty set holds M |= {} WFF
proof
let M be non empty set ; ::_thesis: M |= {} WFF
let H be ZF-formula; :: according to ZFREFLE1:def_1 ::_thesis: ( H in {} WFF implies M |= H )
thus  ( H in {} WFF implies M |= H ) ; ::_thesis: verum
end;

theorem :: ZFREFLE1:2
for M being non empty set
for F1, F2 being Subset of WFF st F1 c= F2 & M |= F2 holds
M |= F1
proof
let M be non empty set ; ::_thesis: for F1, F2 being Subset of WFF st F1 c= F2 & M |= F2 holds
M |= F1
let F1, F2 be Subset of WFF; ::_thesis: ( F1 c= F2 & M |= F2 implies M |= F1 )
assume A1: ( F1 c= F2 & M |= F2 ) ; ::_thesis: M |= F1
let H be ZF-formula; :: according to ZFREFLE1:def_1 ::_thesis: ( H in F1 implies M |= H )
assume  H in F1 ; ::_thesis: M |= H
hence  M |= H by A1, Def1; ::_thesis: verum
end;

theorem :: ZFREFLE1:3
for M being non empty set
for F1, F2 being Subset of WFF st M |= F1 & M |= F2 holds
M |= F1 \/ F2
proof
let M be non empty set ; ::_thesis: for F1, F2 being Subset of WFF st M |= F1 & M |= F2 holds
M |= F1 \/ F2
let F1, F2 be Subset of WFF; ::_thesis: ( M |= F1 & M |= F2 implies M |= F1 \/ F2 )
assume A1: ( M |= F1 & M |= F2 ) ; ::_thesis: M |= F1 \/ F2
let H be ZF-formula; :: according to ZFREFLE1:def_1 ::_thesis: ( H in F1 \/ F2 implies M |= H )
assume  H in F1 \/ F2 ; ::_thesis: M |= H
then  ( H in F1 or H in F2 ) by XBOOLE_0:def_3;
hence  M |= H by A1, Def1; ::_thesis: verum
end;

theorem Th4: :: ZFREFLE1:4
for M being non empty set st M is being_a_model_of_ZF holds
M |= ZF-axioms
proof
let M be non empty set ; ::_thesis: ( M is being_a_model_of_ZF implies M |= ZF-axioms )
assume A1: ( M is epsilon-transitive & M |= the_axiom_of_pairs & M |= the_axiom_of_unions & M |= the_axiom_of_infinity & M |= the_axiom_of_power_sets & ( for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
M |= the_axiom_of_substitution_for H ) ) ; :: according to ZF_MODEL:def_12 ::_thesis: M |= ZF-axioms
let H be ZF-formula; :: according to ZFREFLE1:def_1 ::_thesis: ( H in ZF-axioms implies M |= H )
assume  H in ZF-axioms ; ::_thesis: M |= H
then  ( H = the_axiom_of_extensionality or H = the_axiom_of_pairs or H = the_axiom_of_unions or H = the_axiom_of_infinity or H = the_axiom_of_power_sets or ex H1 being ZF-formula st
( {(x. 0),(x. 1),(x. 2)} misses Free H1 & H = the_axiom_of_substitution_for H1 ) ) by Def4;
hence  M |= H by A1, ZFMODEL1:1; ::_thesis: verum
end;

theorem Th5: :: ZFREFLE1:5
for M being non empty set st M |= ZF-axioms & M is epsilon-transitive holds
M is being_a_model_of_ZF
proof
let M be non empty set ; ::_thesis: ( M |= ZF-axioms & M is epsilon-transitive implies M is being_a_model_of_ZF )
 the_axiom_of_power_sets in WFF by ZF_LANG:4;
then A1: the_axiom_of_power_sets in ZF-axioms by Def4;
 the_axiom_of_infinity in WFF by ZF_LANG:4;
then A2: the_axiom_of_infinity in ZF-axioms by Def4;
 the_axiom_of_unions in WFF by ZF_LANG:4;
then A3: the_axiom_of_unions in ZF-axioms by Def4;
assume that
A4: for H being ZF-formula st H in ZF-axioms holds
M |= H and
A5: M is epsilon-transitive ; :: according to ZFREFLE1:def_1 ::_thesis: M is being_a_model_of_ZF
 the_axiom_of_pairs in WFF by ZF_LANG:4;
then  the_axiom_of_pairs in ZF-axioms by Def4;
hence  ( M is epsilon-transitive & M |= the_axiom_of_pairs & M |= the_axiom_of_unions & M |= the_axiom_of_infinity & M |= the_axiom_of_power_sets ) by A4, A5, A3, A2, A1; :: according to ZF_MODEL:def_12 ::_thesis: for b1 being M7( NAT ) holds
( not {(x. 0),(x. 1),(x. 2)} misses Free b1 or M |= the_axiom_of_substitution_for b1 )
let H be ZF-formula; ::_thesis: ( not {(x. 0),(x. 1),(x. 2)} misses Free H or M |= the_axiom_of_substitution_for H )
assume A6: {(x. 0),(x. 1),(x. 2)} misses Free H ; ::_thesis: M |= the_axiom_of_substitution_for H
 the_axiom_of_substitution_for H in WFF by ZF_LANG:4;
then  the_axiom_of_substitution_for H in ZF-axioms by A6, Def4;
hence  M |= the_axiom_of_substitution_for H by A4; ::_thesis: verum
end;

theorem Th6: :: ZFREFLE1:6
for H being ZF-formula ex S being ZF-formula st
( Free S = {} & ( for M being non empty set holds
( M |= S iff M |= H ) ) )
proof
let H be ZF-formula; ::_thesis: ex S being ZF-formula st
( Free S = {} & ( for M being non empty set holds
( M |= S iff M |= H ) ) )
defpred S2[ Element of NAT ] means  for H being ZF-formula st card (Free H) = $1 holds
ex S being ZF-formula st
( Free S = {} & ( for M being non empty set holds
( M |= S iff M |= H ) ) );
A1: for i being Element of NAT st S2[i] holds
S2[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S2[i] implies S2[i + 1] )
assume A2: S2[i] ; ::_thesis: S2[i + 1]
let H be ZF-formula; ::_thesis: ( card (Free H) = i + 1 implies ex S being ZF-formula st
( Free S = {} & ( for M being non empty set holds
( M |= S iff M |= H ) ) ) )
set e = the Element of Free H;
assume A3: card (Free H) = i + 1 ; ::_thesis: ex S being ZF-formula st
( Free S = {} & ( for M being non empty set holds
( M |= S iff M |= H ) ) )
then A4: Free H <> {} by CARD_1:27, NAT_1:5;
then reconsider x = the Element of Free H as Variable by TARSKI:def_3;
A5: {x} c= Free H by A4, ZFMISC_1:31;
A6: Free (All (x,H)) = (Free H) \ {x} by ZF_LANG1:62;
 x in {x} by ZFMISC_1:31;
then A7: not x in Free (All (x,H)) by A6, XBOOLE_0:def_5;
 (Free (All (x,H))) \/ {x} = (Free H) \/ {x} by A6, XBOOLE_1:39;
then  (Free (All (x,H))) \/ {x} = Free H by A5, XBOOLE_1:12;
then  (card (Free (All (x,H)))) + 1 = card (Free H) by A7, CARD_2:41;
then consider S being ZF-formula such that
A8: Free S = {} and
A9: for M being non empty set holds
( M |= S iff M |= All (x,H) ) by A2, A3, XCMPLX_1:2;
take  S ; ::_thesis: ( Free S = {} & ( for M being non empty set holds
( M |= S iff M |= H ) ) )
thus  Free S = {} by A8; ::_thesis: for M being non empty set holds
( M |= S iff M |= H )
let M be non empty set ; ::_thesis: ( M |= S iff M |= H )
 ( M |= H iff M |= All (x,H) ) by ZF_MODEL:23;
hence  ( M |= S iff M |= H ) by A9; ::_thesis: verum
end;
A10: card (Free H) = card (Free H) ;
A11: S2[ 0 ]
proof
let H be ZF-formula; ::_thesis: ( card (Free H) = 0 implies ex S being ZF-formula st
( Free S = {} & ( for M being non empty set holds
( M |= S iff M |= H ) ) ) )
assume A12: card (Free H) = 0 ; ::_thesis: ex S being ZF-formula st
( Free S = {} & ( for M being non empty set holds
( M |= S iff M |= H ) ) )
take  H ; ::_thesis: ( Free H = {} & ( for M being non empty set holds
( M |= H iff M |= H ) ) )
thus  ( Free H = {} & ( for M being non empty set holds
( M |= H iff M |= H ) ) ) by A12; ::_thesis: verum
end;
 for i being Element of NAT holds S2[i] from NAT_1:sch_1(A11, A1);
hence  ex S being ZF-formula st
( Free S = {} & ( for M being non empty set holds
( M |= S iff M |= H ) ) ) by A10; ::_thesis: verum
end;

theorem :: ZFREFLE1:7
for M1, M2 being non empty set holds
( M1 <==> M2 iff for H being ZF-formula holds
( M1 |= H iff M2 |= H ) )
proof
let M1, M2 be non empty set ; ::_thesis: ( M1 <==> M2 iff for H being ZF-formula holds
( M1 |= H iff M2 |= H ) )
thus  ( M1 <==> M2 implies for H being ZF-formula holds
( M1 |= H iff M2 |= H ) ) ::_thesis: ( ( for H being ZF-formula holds
( M1 |= H iff M2 |= H ) ) implies M1 <==> M2 )
proof
assume A1: for H being ZF-formula st Free H = {} holds
( M1 |= H iff M2 |= H ) ; :: according to ZFREFLE1:def_2 ::_thesis: for H being ZF-formula holds
( M1 |= H iff M2 |= H )
let H be ZF-formula; ::_thesis: ( M1 |= H iff M2 |= H )
consider S being ZF-formula such that
A2: Free S = {} and
A3: for M being non empty set holds
( M |= S iff M |= H ) by Th6;
 ( M1 |= S iff M2 |= S ) by A1, A2;
hence  ( M1 |= H iff M2 |= H ) by A3; ::_thesis: verum
end;
assume A4: for H being ZF-formula holds
( M1 |= H iff M2 |= H ) ; ::_thesis: M1 <==> M2
let H be ZF-formula; :: according to ZFREFLE1:def_2 ::_thesis: ( Free H = {} implies ( M1 |= H iff M2 |= H ) )
thus  ( Free H = {} implies ( M1 |= H iff M2 |= H ) ) by A4; ::_thesis: verum
end;

theorem Th8: :: ZFREFLE1:8
for M1, M2 being non empty set holds
( M1 <==> M2 iff for F being Subset of WFF holds
( M1 |= F iff M2 |= F ) )
proof
let M1, M2 be non empty set ; ::_thesis: ( M1 <==> M2 iff for F being Subset of WFF holds
( M1 |= F iff M2 |= F ) )
thus  ( M1 <==> M2 implies for F being Subset of WFF holds
( M1 |= F iff M2 |= F ) ) ::_thesis: ( ( for F being Subset of WFF holds
( M1 |= F iff M2 |= F ) ) implies M1 <==> M2 )
proof
assume A1: for H being ZF-formula st Free H = {} holds
( M1 |= H iff M2 |= H ) ; :: according to ZFREFLE1:def_2 ::_thesis: for F being Subset of WFF holds
( M1 |= F iff M2 |= F )
let F be Subset of WFF; ::_thesis: ( M1 |= F iff M2 |= F )
thus  ( M1 |= F implies M2 |= F ) ::_thesis: ( M2 |= F implies M1 |= F )
proof
assume A2: for H being ZF-formula st H in F holds
M1 |= H ; :: according to ZFREFLE1:def_1 ::_thesis: M2 |= F
let H be ZF-formula; :: according to ZFREFLE1:def_1 ::_thesis: ( H in F implies M2 |= H )
consider S being ZF-formula such that
A3: Free S = {} and
A4: for M being non empty set holds
( M |= S iff M |= H ) by Th6;
assume  H in F ; ::_thesis: M2 |= H
then  M1 |= H by A2;
then  M1 |= S by A4;
then  M2 |= S by A1, A3;
hence  M2 |= H by A4; ::_thesis: verum
end;
assume A5: for H being ZF-formula st H in F holds
M2 |= H ; :: according to ZFREFLE1:def_1 ::_thesis: M1 |= F
let H be ZF-formula; :: according to ZFREFLE1:def_1 ::_thesis: ( H in F implies M1 |= H )
consider S being ZF-formula such that
A6: Free S = {} and
A7: for M being non empty set holds
( M |= S iff M |= H ) by Th6;
assume  H in F ; ::_thesis: M1 |= H
then  M2 |= H by A5;
then  M2 |= S by A7;
then  M1 |= S by A1, A6;
hence  M1 |= H by A7; ::_thesis: verum
end;
assume A8: for F being Subset of WFF holds
( M1 |= F iff M2 |= F ) ; ::_thesis: M1 <==> M2
let H be ZF-formula; :: according to ZFREFLE1:def_2 ::_thesis: ( Free H = {} implies ( M1 |= H iff M2 |= H ) )
assume  Free H = {} ; ::_thesis: ( M1 |= H iff M2 |= H )
 H in WFF by ZF_LANG:4;
then reconsider F = {H} as Subset of WFF by ZFMISC_1:31;
thus  ( M1 |= H implies M2 |= H ) ::_thesis: ( M2 |= H implies M1 |= H )
proof
assume  M1 |= H ; ::_thesis: M2 |= H
then  for S being ZF-formula st S in F holds
M1 |= S by TARSKI:def_1;
then  M1 |= F by Def1;
then A9: M2 |= F by A8;
 H in F by TARSKI:def_1;
hence  M2 |= H by A9, Def1; ::_thesis: verum
end;
assume  M2 |= H ; ::_thesis: M1 |= H
then  for S being ZF-formula st S in F holds
M2 |= S by TARSKI:def_1;
then  M2 |= F by Def1;
then A10: M1 |= F by A8;
 H in F by TARSKI:def_1;
hence  M1 |= H by A10, Def1; ::_thesis: verum
end;

theorem Th9: :: ZFREFLE1:9
for M1, M2 being non empty set st M1 is_elementary_subsystem_of M2 holds
M1 <==> M2
proof
let M1, M2 be non empty set ; ::_thesis: ( M1 is_elementary_subsystem_of M2 implies M1 <==> M2 )
assume that
 M1 c= M2 and
A1: for H being ZF-formula
for v being Function of VAR,M1 holds
( M1,v |= H iff M2,M2 ! v |= H ) ; :: according to ZFREFLE1:def_3 ::_thesis: M1 <==> M2
let H be ZF-formula; :: according to ZFREFLE1:def_2 ::_thesis: ( Free H = {} implies ( M1 |= H iff M2 |= H ) )
assume A2: Free H = {} ; ::_thesis: ( M1 |= H iff M2 |= H )
thus  ( M1 |= H implies M2 |= H ) ::_thesis: ( M2 |= H implies M1 |= H )
proof
assume A3: for v1 being Function of VAR,M1 holds M1,v1 |= H ; :: according to ZF_MODEL:def_5 ::_thesis: M2 |= H
set v1 = the Function of VAR,M1;
 M1, the Function of VAR,M1 |= H by A3;
then A4: M2,M2 ! the Function of VAR,M1 |= H by A1;
let v2 be Function of VAR,M2; :: according to ZF_MODEL:def_5 ::_thesis: M2,v2 |= H
 for x being Variable st x in Free H holds
v2 . x = (M2 ! the Function of VAR,M1) . x by A2;
hence  M2,v2 |= H by A4, ZF_LANG1:75; ::_thesis: verum
end;
assume A5: for v2 being Function of VAR,M2 holds M2,v2 |= H ; :: according to ZF_MODEL:def_5 ::_thesis: M1 |= H
let v1 be Function of VAR,M1; :: according to ZF_MODEL:def_5 ::_thesis: M1,v1 |= H
 M2,M2 ! v1 |= H by A5;
hence  M1,v1 |= H by A1; ::_thesis: verum
end;

theorem Th10: :: ZFREFLE1:10
for M1, M2 being non empty set st M1 is being_a_model_of_ZF & M1 <==> M2 & M2 is epsilon-transitive holds
M2 is being_a_model_of_ZF
proof
let M1, M2 be non empty set ; ::_thesis: ( M1 is being_a_model_of_ZF & M1 <==> M2 & M2 is epsilon-transitive implies M2 is being_a_model_of_ZF )
assume that
A1: M1 is being_a_model_of_ZF and
A2: M1 <==> M2 ; ::_thesis: ( not M2 is epsilon-transitive or M2 is being_a_model_of_ZF )
 M1 |= ZF-axioms by A1, Th4;
then  M2 |= ZF-axioms by A2, Th8;
hence  ( not M2 is epsilon-transitive or M2 is being_a_model_of_ZF ) by Th5; ::_thesis: verum
end;

theorem Th11: :: ZFREFLE1:11
for f being Function
for W being Universe st dom f in W & rng f c= W holds
rng f in W
proof
let f be Function; ::_thesis: for W being Universe st dom f in W & rng f c= W holds
rng f in W
let W be Universe; ::_thesis: ( dom f in W & rng f c= W implies rng f in W )
assume  dom f in W ; ::_thesis: ( not rng f c= W or rng f in W )
then  ( rng f = f .: (dom f) & card (dom f) in card W ) by CLASSES2:1, RELAT_1:113;
then  card (rng f) in card W by CARD_1:67, ORDINAL1:12;
hence  ( not rng f c= W or rng f in W ) by CLASSES1:1; ::_thesis: verum
end;

theorem :: ZFREFLE1:12
for X, Y being set st ( X,Y are_equipotent or card X = card Y ) holds
( bool X, bool Y are_equipotent & card (bool X) = card (bool Y) )
proof
let X, Y be set ; ::_thesis: ( ( X,Y are_equipotent or card X = card Y ) implies ( bool X, bool Y are_equipotent & card (bool X) = card (bool Y) ) )
assume  ( X,Y are_equipotent or card X = card Y ) ; ::_thesis: ( bool X, bool Y are_equipotent & card (bool X) = card (bool Y) )
then  X,Y are_equipotent by CARD_1:5;
then A1: card (Funcs (X,{0,1})) = card (Funcs (Y,{0,1})) by FUNCT_5:60;
 ( card (Funcs (X,{0,1})) = card (bool X) & card (Funcs (Y,{0,1})) = card (bool Y) ) by FUNCT_5:65;
hence  ( bool X, bool Y are_equipotent & card (bool X) = card (bool Y) ) by A1, CARD_1:5; ::_thesis: verum
end;

theorem Th13: :: ZFREFLE1:13
for W being Universe
for D being non empty set
for Phi being Function of D,(Funcs ((On W),(On W))) st card D in card W holds
ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & phi . (0-element_of W) = 0-element_of W & ( for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ) & ( for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds
phi . a = sup (phi | a) ) )
proof
let W be Universe; ::_thesis: for D being non empty set
for Phi being Function of D,(Funcs ((On W),(On W))) st card D in card W holds
ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & phi . (0-element_of W) = 0-element_of W & ( for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ) & ( for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds
phi . a = sup (phi | a) ) )
deffunc H1( set , T-Sequence) ->  set = sup $2;
let D be non empty set ; ::_thesis: for Phi being Function of D,(Funcs ((On W),(On W))) st card D in card W holds
ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & phi . (0-element_of W) = 0-element_of W & ( for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ) & ( for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds
phi . a = sup (phi | a) ) )
let Phi be Function of D,(Funcs ((On W),(On W))); ::_thesis: ( card D in card W implies ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & phi . (0-element_of W) = 0-element_of W & ( for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ) & ( for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds
phi . a = sup (phi | a) ) ) )
assume A1: card D in card W ; ::_thesis: ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & phi . (0-element_of W) = 0-element_of W & ( for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ) & ( for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds
phi . a = sup (phi | a) ) )
deffunc H2( Ordinal, Ordinal) ->  set = sup ({$2} \/ ((uncurry Phi) .: [:D,{(succ $1)}:]));
consider L being Ordinal-Sequence such that
A2: ( dom L = On W & ( {} in On W implies L . {} = {} ) ) and
A3: for A being Ordinal st succ A in On W holds
L . (succ A) = H2(A,L . A) and
A4: for A being Ordinal st A in On W & A <> {} & A is limit_ordinal holds
L . A = H1(A,L | A) from ORDINAL2:sch_11();
defpred S2[ Ordinal] means L . $1 in On W;
A5: for a being Ordinal of W st S2[a] holds
S2[ succ a]
proof
let a be Ordinal of W; ::_thesis: ( S2[a] implies S2[ succ a] )
A6: On W c= W by ORDINAL2:7;
assume  L . a in On W ; ::_thesis: S2[ succ a]
then reconsider b = L . a as Ordinal of W by ZF_REFLE:7;
 card [:D,{(succ a)}:] = card D by CARD_1:69;
then  card ((uncurry Phi) .: [:D,{(succ a)}:]) c= card D by CARD_1:66;
then A7: card ((uncurry Phi) .: [:D,{(succ a)}:]) in card W by A1, ORDINAL1:12;
 rng Phi c= Funcs ((On W),(On W)) by RELAT_1:def_19;
then A8: rng (uncurry Phi) c= On W by FUNCT_5:41;
 (uncurry Phi) .: [:D,{(succ a)}:] c= rng (uncurry Phi) by RELAT_1:111;
then  (uncurry Phi) .: [:D,{(succ a)}:] c= On W by A8, XBOOLE_1:1;
then  (uncurry Phi) .: [:D,{(succ a)}:] c= W by A6, XBOOLE_1:1;
then  (uncurry Phi) .: [:D,{(succ a)}:] in W by A7, CLASSES1:1;
then A9: {b} \/ ((uncurry Phi) .: [:D,{(succ a)}:]) in W by CLASSES2:60;
 succ a in On W by ZF_REFLE:7;
then  L . (succ a) = sup ({b} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) by A3;
then  L . (succ a) in W by A9, ZF_REFLE:19;
hence  S2[ succ a] by ORDINAL1:def_9; ::_thesis: verum
end;
A10: for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal & ( for b being Ordinal of W st b in a holds
S2[b] ) holds
S2[a]
proof
let a be Ordinal of W; ::_thesis: ( a <> 0-element_of W & a is limit_ordinal & ( for b being Ordinal of W st b in a holds
S2[b] ) implies S2[a] )
assume that
A11: ( a <> 0-element_of W & a is limit_ordinal ) and
A12: for b being Ordinal of W st b in a holds
L . b in On W ; ::_thesis: S2[a]
A13: dom (L | a) c= a by RELAT_1:58;
then A14: dom (L | a) in W by CLASSES1:def_1;
A15: a in On W by ZF_REFLE:7;
A16: rng (L | a) c= W
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in rng (L | a) or e in W )
assume  e in rng (L | a) ; ::_thesis: e in W
then consider u being set  such that
A17: u in dom (L | a) and
A18: e = (L | a) . u by FUNCT_1:def_3;
reconsider u = u as Ordinal by A17;
 u in On W by A15, A13, A17, ORDINAL1:10;
then reconsider u = u as Ordinal of W by ZF_REFLE:7;
 e = L . u by A17, A18, FUNCT_1:47;
then  e in On W by A12, A13, A17;
hence  e in W by ORDINAL1:def_9; ::_thesis: verum
end;
 L . a = sup (L | a) by A4, A11, A15;
then  L . a in W by A14, A16, Th11, ZF_REFLE:19;
hence  S2[a] by ORDINAL1:def_9; ::_thesis: verum
end;
A19: S2[ 0-element_of W] by A2, ORDINAL1:def_9;
 rng L c= On W
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in rng L or e in On W )
assume  e in rng L ; ::_thesis: e in On W
then consider u being set  such that
A20: u in dom L and
A21: e = L . u by FUNCT_1:def_3;
reconsider u = u as Ordinal of W by A2, A20, ZF_REFLE:7;
 for a being Ordinal of W holds S2[a] from ZF_REFLE:sch_4(A19, A5, A10);
then  L . u in On W ;
hence  e in On W by A21; ::_thesis: verum
end;
then reconsider phi = L as Ordinal-Sequence of W by A2, FUNCT_2:def_1, RELSET_1:4;
take  phi ; ::_thesis: ( phi is increasing & phi is continuous & phi . (0-element_of W) = 0-element_of W & ( for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ) & ( for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds
phi . a = sup (phi | a) ) )
thus A22: phi is increasing ::_thesis: ( phi is continuous & phi . (0-element_of W) = 0-element_of W & ( for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ) & ( for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds
phi . a = sup (phi | a) ) )
proof
let A be Ordinal; :: according to ORDINAL2:def_12 ::_thesis: for b1 being set holds
( not A in b1 or not b1 in dom phi or phi . A in phi . b1 )
let B be Ordinal; ::_thesis: ( not A in B or not B in dom phi or phi . A in phi . B )
assume that
A23: A in B and
A24: B in dom phi ; ::_thesis: phi . A in phi . B
 A in dom phi by A23, A24, ORDINAL1:10;
then reconsider a = A, b = B as Ordinal of W by A2, A24, ZF_REFLE:7;
defpred S3[ Ordinal] means ( a in $1 implies phi . a in phi . $1 );
A25: for b being Ordinal of W st S3[b] holds
S3[ succ b]
proof
let b be Ordinal of W; ::_thesis: ( S3[b] implies S3[ succ b] )
assume A26: ( ( a in b implies phi . a in phi . b ) & a in succ b ) ; ::_thesis: phi . a in phi . (succ b)
 phi . b in {(phi . b)} by TARSKI:def_1;
then A27: phi . b in {(phi . b)} \/ ((uncurry Phi) .: [:D,{(succ b)}:]) by XBOOLE_0:def_3;
 succ b in On W by ZF_REFLE:7;
then  phi . (succ b) = sup ({(phi . b)} \/ ((uncurry Phi) .: [:D,{(succ b)}:])) by A3;
then  phi . b in phi . (succ b) by A27, ORDINAL2:19;
hence  phi . a in phi . (succ b) by A26, ORDINAL1:8, ORDINAL1:10; ::_thesis: verum
end;
A28: for b being Ordinal of W st b <> 0-element_of W & b is limit_ordinal & ( for c being Ordinal of W st c in b holds
S3[c] ) holds
S3[b]
proof
let b be Ordinal of W; ::_thesis: ( b <> 0-element_of W & b is limit_ordinal & ( for c being Ordinal of W st c in b holds
S3[c] ) implies S3[b] )
assume that
A29: ( b <> 0-element_of W & b is limit_ordinal ) and
 for c being Ordinal of W st c in b & a in c holds
phi . a in phi . c and
A30: a in b ; ::_thesis: phi . a in phi . b
 b in On W by ZF_REFLE:7;
then A31: phi . b = sup (phi | b) by A4, A29;
 a in On W by ZF_REFLE:7;
then  phi . a in rng (phi | b) by A2, A30, FUNCT_1:50;
hence  phi . a in phi . b by A31, ORDINAL2:19; ::_thesis: verum
end;
A32: S3[ 0-element_of W] ;
 for b being Ordinal of W holds S3[b] from ZF_REFLE:sch_4(A32, A25, A28);
then  phi . a in phi . b by A23;
hence  phi . A in phi . B ; ::_thesis: verum
end;
thus  phi is continuous ::_thesis: ( phi . (0-element_of W) = 0-element_of W & ( for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ) & ( for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds
phi . a = sup (phi | a) ) )
proof
let A be Ordinal; :: according to ORDINAL2:def_13 ::_thesis: for b1 being set holds
( not A in dom phi or A = {} or not A is limit_ordinal or not b1 = phi . A or b1 is_limes_of phi | A )
let B be Ordinal; ::_thesis: ( not A in dom phi or A = {} or not A is limit_ordinal or not B = phi . A or B is_limes_of phi | A )
assume that
A33: A in dom phi and
A34: ( A <> {} & A is limit_ordinal ) and
A35: B = phi . A ; ::_thesis: B is_limes_of phi | A
 A c= dom phi by A33, ORDINAL1:def_2;
then A36: dom (phi | A) = A by RELAT_1:62;
A37: phi | A is increasing by A22, ORDINAL4:15;
 B = sup (phi | A) by A2, A4, A33, A34, A35;
hence  B is_limes_of phi | A by A34, A36, A37, ORDINAL4:8; ::_thesis: verum
end;
thus  phi . (0-element_of W) = 0-element_of W by A2, ORDINAL1:def_9; ::_thesis: ( ( for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ) & ( for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds
phi . a = sup (phi | a) ) )
thus  for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ::_thesis: for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds
phi . a = sup (phi | a)
proof
let a be Ordinal of W; ::_thesis: phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:]))
 succ a in On W by ZF_REFLE:7;
hence  phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) by A3; ::_thesis: verum
end;
let a be Ordinal of W; ::_thesis: ( a <> 0-element_of W & a is limit_ordinal implies phi . a = sup (phi | a) )
 a in On W by ZF_REFLE:7;
hence  ( a <> 0-element_of W & a is limit_ordinal implies phi . a = sup (phi | a) ) by A4; ::_thesis: verum
end;

theorem Th14: :: ZFREFLE1:14
for C being Ordinal
for phi being Ordinal-Sequence st phi is increasing holds
C +^ phi is increasing
proof
let C be Ordinal; ::_thesis: for phi being Ordinal-Sequence st phi is increasing holds
C +^ phi is increasing
let phi be Ordinal-Sequence; ::_thesis: ( phi is increasing implies C +^ phi is increasing )
assume A1: phi is increasing ; ::_thesis: C +^ phi is increasing
let A be Ordinal; :: according to ORDINAL2:def_12 ::_thesis: for b1 being set holds
( not A in b1 or not b1 in dom (C +^ phi) or (C +^ phi) . A in (C +^ phi) . b1 )
let B be Ordinal; ::_thesis: ( not A in B or not B in dom (C +^ phi) or (C +^ phi) . A in (C +^ phi) . B )
set xi = C +^ phi;
assume that
A2: A in B and
A3: B in dom (C +^ phi) ; ::_thesis: (C +^ phi) . A in (C +^ phi) . B
reconsider A9 = phi . A, B9 = phi . B as Ordinal ;
A4: dom (C +^ phi) = dom phi by ORDINAL3:def_1;
then A5: (C +^ phi) . B = C +^ B9 by A3, ORDINAL3:def_1;
 A in dom (C +^ phi) by A2, A3, ORDINAL1:10;
then A6: (C +^ phi) . A = C +^ A9 by A4, ORDINAL3:def_1;
 A9 in B9 by A1, A2, A3, A4, ORDINAL2:def_12;
hence  (C +^ phi) . A in (C +^ phi) . B by A6, A5, ORDINAL2:32; ::_thesis: verum
end;

theorem Th15: :: ZFREFLE1:15
for C, A being Ordinal
for xi being Ordinal-Sequence holds (C +^ xi) | A = C +^ (xi | A)
proof
let C, A be Ordinal; ::_thesis: for xi being Ordinal-Sequence holds (C +^ xi) | A = C +^ (xi | A)
let xi be Ordinal-Sequence; ::_thesis: (C +^ xi) | A = C +^ (xi | A)
A1: dom (xi | A) = (dom xi) /\ A by RELAT_1:61;
A2: dom (C +^ xi) = dom xi by ORDINAL3:def_1;
A3: dom ((C +^ xi) | A) = (dom (C +^ xi)) /\ A by RELAT_1:61;
A4: now__::_thesis:_for_e_being_set_st_e_in_dom_((C_+^_xi)_|_A)_holds_
((C_+^_xi)_|_A)_._e_=_(C_+^_(xi_|_A))_._e
let e be set ; ::_thesis: ( e in dom ((C +^ xi) | A) implies ((C +^ xi) | A) . e = (C +^ (xi | A)) . e )
assume A5: e in dom ((C +^ xi) | A) ; ::_thesis: ((C +^ xi) | A) . e = (C +^ (xi | A)) . e
then reconsider a = e as Ordinal ;
A6: e in dom xi by A3, A2, A5, XBOOLE_0:def_4;
thus ((C +^ xi) | A) . e = (C +^ xi) . a by A5, FUNCT_1:47
.= C +^ (xi . a) by A6, ORDINAL3:def_1
.= C +^ ((xi | A) . a) by A3, A1, A2, A5, FUNCT_1:47
.= (C +^ (xi | A)) . e by A3, A1, A2, A5, ORDINAL3:def_1 ; ::_thesis: verum
end;
 dom (C +^ (xi | A)) = dom (xi | A) by ORDINAL3:def_1;
hence  (C +^ xi) | A = C +^ (xi | A) by A1, A2, A4, FUNCT_1:2, RELAT_1:61; ::_thesis: verum
end;

theorem Th16: :: ZFREFLE1:16
for C being Ordinal
for phi being Ordinal-Sequence st phi is increasing & phi is continuous holds
C +^ phi is continuous
proof
let C be Ordinal; ::_thesis: for phi being Ordinal-Sequence st phi is increasing & phi is continuous holds
C +^ phi is continuous
let phi be Ordinal-Sequence; ::_thesis: ( phi is increasing & phi is continuous implies C +^ phi is continuous )
assume A1: phi is increasing ; ::_thesis: ( not phi is continuous or C +^ phi is continuous )
assume A2: for A, B being Ordinal st A in dom phi & A <> {} & A is limit_ordinal & B = phi . A holds
B is_limes_of phi | A ; :: according to ORDINAL2:def_13 ::_thesis: C +^ phi is continuous
let A be Ordinal; :: according to ORDINAL2:def_13 ::_thesis: for b1 being set holds
( not A in dom (C +^ phi) or A = {} or not A is limit_ordinal or not b1 = (C +^ phi) . A or b1 is_limes_of (C +^ phi) | A )
let B be Ordinal; ::_thesis: ( not A in dom (C +^ phi) or A = {} or not A is limit_ordinal or not B = (C +^ phi) . A or B is_limes_of (C +^ phi) | A )
set xi = phi | A;
reconsider A9 = phi . A as Ordinal ;
assume that
A3: A in dom (C +^ phi) and
A4: A <> {} and
A5: A is limit_ordinal and
A6: B = (C +^ phi) . A ; ::_thesis: B is_limes_of (C +^ phi) | A
A7: dom phi = dom (C +^ phi) by ORDINAL3:def_1;
then A8: B = C +^ A9 by A3, A6, ORDINAL3:def_1;
 A9 is_limes_of phi | A by A2, A3, A4, A5, A7;
then A9: lim (phi | A) = A9 by ORDINAL2:def_10;
A10: ( dom (phi | A) = dom (C +^ (phi | A)) & (C +^ phi) | A = C +^ (phi | A) ) by Th15, ORDINAL3:def_1;
A11: phi | A is increasing by A1, ORDINAL4:15;
then A12: C +^ (phi | A) is increasing by Th14;
 A c= dom (C +^ phi) by A3, ORDINAL1:def_2;
then A13: dom (phi | A) = A by A7, RELAT_1:62;
then A14: sup (C +^ (phi | A)) = C +^ (sup (phi | A)) by A4, ORDINAL3:43;
 sup (phi | A) = lim (phi | A) by A4, A5, A13, A11, ORDINAL4:8;
hence  B is_limes_of (C +^ phi) | A by A4, A5, A13, A10, A8, A14, A9, A12, ORDINAL4:8; ::_thesis: verum
end;

theorem :: ZFREFLE1:17
for e being set
for psi being Ordinal-Sequence st e in rng psi holds
e is Ordinal by ORDINAL2:48;

theorem :: ZFREFLE1:18
for psi being Ordinal-Sequence holds rng psi c= sup psi by ORDINAL2:49;

theorem :: ZFREFLE1:19
for A, B, C being Ordinal st A is_cofinal_with B & B is_cofinal_with C holds
A is_cofinal_with C by ORDINAL4:37;

theorem Th20: :: ZFREFLE1:20
for A, B being Ordinal st A is_cofinal_with B holds
B c= A
proof
let A, B be Ordinal; ::_thesis: ( A is_cofinal_with B implies B c= A )
given psi being Ordinal-Sequence such that A1: dom psi = B and
A2: rng psi c= A and
A3: psi is increasing and
 A = sup psi ; :: according to ORDINAL2:def_17 ::_thesis: B c= A
let C be Ordinal; :: according to ORDINAL1:def_5 ::_thesis: ( not C in B or C in A )
assume  C in B ; ::_thesis: C in A
then  ( C c= psi . C & psi . C in rng psi ) by A1, A3, FUNCT_1:def_3, ORDINAL4:10;
hence  C in A by A2, ORDINAL1:12; ::_thesis: verum
end;

theorem :: ZFREFLE1:21
for A, B being Ordinal st A is_cofinal_with B & B is_cofinal_with A holds
A = B
proof
let A, B be Ordinal; ::_thesis: ( A is_cofinal_with B & B is_cofinal_with A implies A = B )
assume  ( A is_cofinal_with B & B is_cofinal_with A ) ; ::_thesis: A = B
hence  ( A c= B & B c= A ) by Th20; :: according to XBOOLE_0:def_10 ::_thesis: verum
end;

theorem :: ZFREFLE1:22
for A being Ordinal
for psi being Ordinal-Sequence st dom psi <> {} & dom psi is limit_ordinal & psi is increasing & A is_limes_of psi holds
A is_cofinal_with dom psi
proof
let A be Ordinal; ::_thesis: for psi being Ordinal-Sequence st dom psi <> {} & dom psi is limit_ordinal & psi is increasing & A is_limes_of psi holds
A is_cofinal_with dom psi
let psi be Ordinal-Sequence; ::_thesis: ( dom psi <> {} & dom psi is limit_ordinal & psi is increasing & A is_limes_of psi implies A is_cofinal_with dom psi )
assume that
A1: ( dom psi <> {} & dom psi is limit_ordinal ) and
A2: psi is increasing and
A3: A is_limes_of psi ; ::_thesis: A is_cofinal_with dom psi
take  psi ; :: according to ORDINAL2:def_17 ::_thesis: ( dom psi = dom psi & rng psi c= A & psi is increasing & A = sup psi )
thus  dom psi = dom psi ; ::_thesis: ( rng psi c= A & psi is increasing & A = sup psi )
 ( sup psi = lim psi & A = lim psi ) by A1, A2, A3, ORDINAL2:def_10, ORDINAL4:8;
hence  ( rng psi c= A & psi is increasing & A = sup psi ) by A2, ORDINAL2:49; ::_thesis: verum
end;

theorem :: ZFREFLE1:23
for A being Ordinal holds succ A is_cofinal_with 1 by ORDINAL3:73;

theorem :: ZFREFLE1:24
for A, B being Ordinal st A is_cofinal_with succ B holds
ex C being Ordinal st A = succ C
proof
let A, B be Ordinal; ::_thesis: ( A is_cofinal_with succ B implies ex C being Ordinal st A = succ C )
given psi being Ordinal-Sequence such that A1: dom psi = succ B and
A2: rng psi c= A and
A3: psi is increasing and
A4: A = sup psi ; :: according to ORDINAL2:def_17 ::_thesis: ex C being Ordinal st A = succ C
reconsider C = psi . B as Ordinal ;
take  C ; ::_thesis: A = succ C
thus  A c= succ C :: according to XBOOLE_0:def_10 ::_thesis: succ C c= A
proof
let a be Ordinal; :: according to ORDINAL1:def_5 ::_thesis: ( not a in A or a in succ C )
assume  a in A ; ::_thesis: a in succ C
then consider b being Ordinal such that
A5: b in rng psi and
A6: a c= b by A4, ORDINAL2:21;
consider e being set  such that
A7: e in succ B and
A8: b = psi . e by A1, A5, FUNCT_1:def_3;
reconsider e = e as Ordinal by A7;
 e c= B by A7, ORDINAL1:22;
then  b c= C by A1, A3, A8, ORDINAL1:6, ORDINAL4:9;
then  b in succ C by ORDINAL1:22;
hence  a in succ C by A6, ORDINAL1:12; ::_thesis: verum
end;
 B in succ B by ORDINAL1:6;
then  C in rng psi by A1, FUNCT_1:def_3;
hence  succ C c= A by A2, ORDINAL1:21; ::_thesis: verum
end;

theorem :: ZFREFLE1:25
for A, B being Ordinal st A is_cofinal_with B holds
( A is limit_ordinal iff B is limit_ordinal ) by ORDINAL4:38;

theorem :: ZFREFLE1:26
for A being Ordinal st A is_cofinal_with {} holds
A = {} by ORDINAL2:50;

theorem :: ZFREFLE1:27
for W being Universe
for a being Ordinal of W holds not On W is_cofinal_with a
proof
let W be Universe; ::_thesis: for a being Ordinal of W holds not On W is_cofinal_with a
let a be Ordinal of W; ::_thesis: not On W is_cofinal_with a
given psi being Ordinal-Sequence such that A1: dom psi = a and
A2: rng psi c= On W and
 psi is increasing and
A3: On W = sup psi ; :: according to ORDINAL2:def_17 ::_thesis: contradiction
 On W c= W by ORDINAL2:7;
then  rng psi c= W by A2, XBOOLE_1:1;
then  sup (rng psi) in W by A1, Th11, ZF_REFLE:19;
then  sup psi in On W by ORDINAL1:def_9;
hence  contradiction by A3; ::_thesis: verum
end;

theorem Th28: :: ZFREFLE1:28
for W being Universe
for a being Ordinal of W
for phi being Ordinal-Sequence of W st omega in W & phi is increasing & phi is continuous holds
ex b being Ordinal of W st
( a in b & phi . b = b )
proof
let W be Universe; ::_thesis: for a being Ordinal of W
for phi being Ordinal-Sequence of W st omega in W & phi is increasing & phi is continuous holds
ex b being Ordinal of W st
( a in b & phi . b = b )
let a be Ordinal of W; ::_thesis: for phi being Ordinal-Sequence of W st omega in W & phi is increasing & phi is continuous holds
ex b being Ordinal of W st
( a in b & phi . b = b )
let phi be Ordinal-Sequence of W; ::_thesis: ( omega in W & phi is increasing & phi is continuous implies ex b being Ordinal of W st
( a in b & phi . b = b ) )
assume that
A1: omega in W and
A2: phi is increasing and
A3: phi is continuous ; ::_thesis: ex b being Ordinal of W st
( a in b & phi . b = b )
deffunc H1( Ordinal of W) ->  Element of W = (succ a) +^ (phi . $1);
consider xi being Ordinal-Sequence of W such that
A4: for b being Ordinal of W holds xi . b = H1(b) from ORDINAL4:sch_2();
A5: dom xi = On W by FUNCT_2:def_1;
A6: dom phi = On W by FUNCT_2:def_1;
 for A being Ordinal st A in dom phi holds
xi . A = (succ a) +^ (phi . A)
proof
let A be Ordinal; ::_thesis: ( A in dom phi implies xi . A = (succ a) +^ (phi . A) )
assume  A in dom phi ; ::_thesis: xi . A = (succ a) +^ (phi . A)
then reconsider b = A as Ordinal of W by A6, ZF_REFLE:7;
 xi . b = (succ a) +^ (phi . b) by A4;
hence  xi . A = (succ a) +^ (phi . A) ; ::_thesis: verum
end;
then  xi = (succ a) +^ phi by A6, A5, ORDINAL3:def_1;
then  ( xi is increasing & xi is continuous ) by A2, A3, Th14, Th16;
then consider A being Ordinal such that
A7: A in dom xi and
A8: xi . A = A by A1, ORDINAL4:36;
reconsider b = A as Ordinal of W by A5, A7, ZF_REFLE:7;
A9: b = (succ a) +^ (phi . b) by A4, A8;
take  b ; ::_thesis: ( a in b & phi . b = b )
A10: ( succ a c= (succ a) +^ (phi . b) & a in succ a ) by ORDINAL1:6, ORDINAL3:24;
A11: phi . b c= (succ a) +^ (phi . b) by ORDINAL3:24;
 b c= phi . b by A2, A6, A5, A7, ORDINAL4:10;
hence  ( a in b & phi . b = b ) by A10, A9, A11, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th29: :: ZFREFLE1:29
for W being Universe
for b being Ordinal of W
for phi being Ordinal-Sequence of W st omega in W & phi is increasing & phi is continuous holds
ex a being Ordinal of W st
( b in a & phi . a = a & a is_cofinal_with omega )
proof
let W be Universe; ::_thesis: for b being Ordinal of W
for phi being Ordinal-Sequence of W st omega in W & phi is increasing & phi is continuous holds
ex a being Ordinal of W st
( b in a & phi . a = a & a is_cofinal_with omega )
let b be Ordinal of W; ::_thesis: for phi being Ordinal-Sequence of W st omega in W & phi is increasing & phi is continuous holds
ex a being Ordinal of W st
( b in a & phi . a = a & a is_cofinal_with omega )
let phi be Ordinal-Sequence of W; ::_thesis: ( omega in W & phi is increasing & phi is continuous implies ex a being Ordinal of W st
( b in a & phi . a = a & a is_cofinal_with omega ) )
assume that
A1: omega in W and
A2: phi is increasing and
A3: phi is continuous ; ::_thesis: ex a being Ordinal of W st
( b in a & phi . a = a & a is_cofinal_with omega )
A4: omega in On W by A1, ORDINAL1:def_9;
deffunc H1( Ordinal, set ) ->  Element of W = 0-element_of W;
deffunc H2( Ordinal, Ordinal of W) ->  Element of W = succ (phi . $2);
consider nu being Ordinal-Sequence of W such that
A5: nu . (0-element_of W) = b and
A6: for a being Ordinal of W holds nu . (succ a) = H2(a,nu . a) and
 for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds
nu . a = H1(a,nu | a) from ZF_REFLE:sch_3();
set xi = nu | omega;
set a = sup (nu | omega);
A7: On W c= W by ORDINAL2:7;
 dom nu = On W by FUNCT_2:def_1;
then A8: omega c= dom nu by A4;
then A9: dom (nu | omega) = omega by RELAT_1:62;
 ( rng (nu | omega) c= rng nu & rng nu c= On W ) by RELAT_1:def_19;
then  rng (nu | omega) c= On W by XBOOLE_1:1;
then  rng (nu | omega) c= W by A7, XBOOLE_1:1;
then reconsider a = sup (nu | omega) as Ordinal of W by A1, A9, Th11, ZF_REFLE:19;
A10: a in dom phi by ORDINAL4:34;
then A11: a c= dom phi by ORDINAL1:def_2;
then A12: dom (phi | a) = a by RELAT_1:62;
A13: nu | omega is increasing
proof
let A be Ordinal; :: according to ORDINAL2:def_12 ::_thesis: for b1 being set holds
( not A in b1 or not b1 in dom (nu | omega) or (nu | omega) . A in (nu | omega) . b1 )
let B be Ordinal; ::_thesis: ( not A in B or not B in dom (nu | omega) or (nu | omega) . A in (nu | omega) . B )
assume that
A14: A in B and
A15: B in dom (nu | omega) ; ::_thesis: (nu | omega) . A in (nu | omega) . B
defpred S2[ Ordinal] means ( A +^ $1 in dom (nu | omega) & $1 <> {} implies (nu | omega) . A in (nu | omega) . (A +^ $1) );
A16: for B being Ordinal st B <> {} & B is limit_ordinal & ( for C being Ordinal st C in B holds
S2[C] ) holds
S2[B]
proof
let B be Ordinal; ::_thesis: ( B <> {} & B is limit_ordinal & ( for C being Ordinal st C in B holds
S2[C] ) implies S2[B] )
assume that
A17: B <> {} and
A18: B is limit_ordinal ; ::_thesis: ( ex C being Ordinal st
( C in B & not S2[C] ) or S2[B] )
 {} in B by A17, ORDINAL3:8;
then A19: omega c= B by A18, ORDINAL1:def_11;
 B c= A +^ B by ORDINAL3:24;
hence  ( ex C being Ordinal st
( C in B & not S2[C] ) or S2[B] ) by A9, A19, ORDINAL1:5; ::_thesis: verum
end;
A20: for C being Ordinal st S2[C] holds
S2[ succ C]
proof
let C be Ordinal; ::_thesis: ( S2[C] implies S2[ succ C] )
assume that
A21: ( A +^ C in dom (nu | omega) & C <> {} implies (nu | omega) . A in (nu | omega) . (A +^ C) ) and
A22: A +^ (succ C) in dom (nu | omega) and
 succ C <> {} ; ::_thesis: (nu | omega) . A in (nu | omega) . (A +^ (succ C))
A23: A +^ (succ C) in On W by A4, A9, A22, ORDINAL1:10;
then reconsider asc = A +^ (succ C) as Ordinal of W by ZF_REFLE:7;
A24: A +^ C in asc by ORDINAL1:6, ORDINAL2:32;
then  A +^ C in On W by A23, ORDINAL1:10;
then reconsider ac = A +^ C as Ordinal of W by ZF_REFLE:7;
A25: now__::_thesis:_(_C_=_{}_implies_(nu_|_omega)_._A_in_(nu_|_omega)_._(A_+^_(succ_C))_)
 nu . ac in dom phi by ORDINAL4:34;
then A26: nu . ac c= phi . (nu . ac) by A2, ORDINAL4:10;
 asc = succ ac by ORDINAL2:28;
then A27: nu . asc = succ (phi . (nu . ac)) by A6;
assume  C = {} ; ::_thesis: (nu | omega) . A in (nu | omega) . (A +^ (succ C))
then A28: ac = A by ORDINAL2:27;
 ( (nu | omega) . ac = nu . ac & (nu | omega) . asc = nu . asc ) by A22, A24, FUNCT_1:47, ORDINAL1:10;
hence  (nu | omega) . A in (nu | omega) . (A +^ (succ C)) by A28, A27, A26, ORDINAL1:6, ORDINAL1:12; ::_thesis: verum
end;
A29: ( succ ac = asc & nu . ac in dom phi ) by ORDINAL2:28, ORDINAL4:34;
 A +^ C in dom (nu | omega) by A22, A24, ORDINAL1:10;
then  ( ( (nu | omega) . A in (nu | omega) . ac & nu . asc = succ (phi . (nu . ac)) & nu . ac = (nu | omega) . ac & phi . (nu . ac) in succ (phi . (nu . ac)) & nu . ac c= phi . (nu . ac) ) or C = {} ) by A2, A6, A21, A29, FUNCT_1:47, ORDINAL1:6, ORDINAL4:10;
then  ( ( (nu | omega) . A in nu . ac & nu . ac in nu . asc & nu . asc = (nu | omega) . asc ) or C = {} ) by A22, FUNCT_1:47, ORDINAL1:12;
then  ( ( (nu | omega) . A in nu . ac & nu . ac c= (nu | omega) . asc ) or C = {} ) by ORDINAL1:def_2;
hence  (nu | omega) . A in (nu | omega) . (A +^ (succ C)) by A25; ::_thesis: verum
end;
A30: S2[ {} ] ;
A31: for C being Ordinal holds S2[C] from ORDINAL2:sch_1(A30, A20, A16);
 ex C being Ordinal st
( B = A +^ C & C <> {} ) by A14, ORDINAL3:28;
hence  (nu | omega) . A in (nu | omega) . B by A15, A31; ::_thesis: verum
end;
then A32: a is limit_ordinal by A9, Lm2, ORDINAL4:16;
take  a ; ::_thesis: ( b in a & phi . a = a & a is_cofinal_with omega )
 0-element_of W in dom nu by ORDINAL4:34;
then A33: b in rng (nu | omega) by A5, Lm1, FUNCT_1:50;
hence  b in a by ORDINAL2:19; ::_thesis: ( phi . a = a & a is_cofinal_with omega )
A34: a <> {} by A33, ORDINAL2:19;
 a in dom phi by ORDINAL4:34;
then A35: phi . a is_limes_of phi | a by A3, A32, A34, ORDINAL2:def_13;
 phi | a is increasing by A2, ORDINAL4:15;
then  sup (phi | a) = lim (phi | a) by A32, A34, A12, ORDINAL4:8;
then A36: phi . a = sup (rng (phi | a)) by A35, ORDINAL2:def_10;
thus  phi . a c= a :: according to XBOOLE_0:def_10 ::_thesis: ( a c= phi . a & a is_cofinal_with omega )
proof
let A be Ordinal; :: according to ORDINAL1:def_5 ::_thesis: ( not A in phi . a or A in a )
assume  A in phi . a ; ::_thesis: A in a
then consider B being Ordinal such that
A37: B in rng (phi | a) and
A38: A c= B by A36, ORDINAL2:21;
consider e being set  such that
A39: e in a and
A40: B = (phi | a) . e by A12, A37, FUNCT_1:def_3;
reconsider e = e as Ordinal by A39;
consider C being Ordinal such that
A41: C in rng (nu | omega) and
A42: e c= C by A39, ORDINAL2:21;
A43: ( e c< C iff ( e c= C & e <> C ) ) by XBOOLE_0:def_8;
consider u being set  such that
A44: u in omega and
A45: C = (nu | omega) . u by A9, A41, FUNCT_1:def_3;
reconsider u = u as Ordinal by A44;
 u c= omega by A44, ORDINAL1:def_2;
then reconsider u = u as Ordinal of W by A1, CLASSES1:def_1;
A46: succ u in dom nu by ORDINAL4:34;
 C in a by A41, ORDINAL2:19;
then  ( e = C or ( e in C & C in dom phi ) ) by A11, A42, A43, ORDINAL1:11;
then A47: ( phi . e = phi . C or phi . e in phi . C ) by A2, ORDINAL2:def_12;
A48: nu . (succ u) = succ (phi . (nu . u)) by A6;
 succ u in omega by A44, Lm2, ORDINAL1:28;
then  nu . (succ u) in rng (nu | omega) by A46, FUNCT_1:50;
then A49: nu . (succ u) in a by ORDINAL2:19;
 C = nu . u by A9, A44, A45, FUNCT_1:47;
then A50: phi . e c= phi . (nu . u) by A47, ORDINAL1:def_2;
 phi . e = B by A12, A39, A40, FUNCT_1:47;
then  B in nu . (succ u) by A48, A50, ORDINAL1:6, ORDINAL1:12;
then  B in a by A49, ORDINAL1:10;
hence  A in a by A38, ORDINAL1:12; ::_thesis: verum
end;
thus  a c= phi . a by A2, A10, ORDINAL4:10; ::_thesis: a is_cofinal_with omega
take  nu | omega ; :: according to ORDINAL2:def_17 ::_thesis: ( dom (nu | omega) = omega & rng (nu | omega) c= a & nu | omega is increasing & a = sup (nu | omega) )
 rng (nu | omega) c= a
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in rng (nu | omega) or e in a )
assume A51: e in rng (nu | omega) ; ::_thesis: e in a
then consider u being set  such that
A52: u in dom (nu | omega) and
A53: e = (nu | omega) . u by FUNCT_1:def_3;
thus  e in a by A51, A52, A53, ORDINAL2:19; ::_thesis: verum
end;
hence  ( dom (nu | omega) = omega & rng (nu | omega) c= a & nu | omega is increasing & a = sup (nu | omega) ) by A8, A13, RELAT_1:62; ::_thesis: verum
end;

theorem Th30: :: ZFREFLE1:30
for W being Universe
for L being DOMAIN-Sequence of W st omega in W & ( for a, b being Ordinal of W st a in b holds
L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds
L . a = Union (L | a) ) holds
ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
L . a is_elementary_subsystem_of Union L ) )
proof
let W be Universe; ::_thesis: for L being DOMAIN-Sequence of W st omega in W & ( for a, b being Ordinal of W st a in b holds
L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds
L . a = Union (L | a) ) holds
ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
L . a is_elementary_subsystem_of Union L ) )
let L be DOMAIN-Sequence of W; ::_thesis: ( omega in W & ( for a, b being Ordinal of W st a in b holds
L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds
L . a = Union (L | a) ) implies ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
L . a is_elementary_subsystem_of Union L ) ) )
assume that
A1: omega in W and
A2: ( ( for a, b being Ordinal of W st a in b holds
L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds
L . a = Union (L | a) ) ) ; ::_thesis: ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
L . a is_elementary_subsystem_of Union L ) )
set M = Union L;
defpred S2[ set , set ] means  ex H being ZF-formula ex phi being Ordinal-Sequence of W st
( $1 = H & $2 = phi & phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
for va being Function of VAR,(L . a) holds
( Union L,(Union L) ! va |= H iff L . a,va |= H ) ) );
A3: for e being set st e in WFF holds
ex u being set st
( u in Funcs ((On W),(On W)) & S2[e,u] )
proof
let e be set ; ::_thesis: ( e in WFF implies ex u being set st
( u in Funcs ((On W),(On W)) & S2[e,u] ) )
assume  e in WFF ; ::_thesis: ex u being set st
( u in Funcs ((On W),(On W)) & S2[e,u] )
then reconsider H = e as ZF-formula by ZF_LANG:4;
consider phi being Ordinal-Sequence of W such that
A4: ( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
for va being Function of VAR,(L . a) holds
( Union L,(Union L) ! va |= H iff L . a,va |= H ) ) ) by A1, A2, ZF_REFLE:20;
reconsider u = phi as set ;
take  u ; ::_thesis: ( u in Funcs ((On W),(On W)) & S2[e,u] )
 ( dom phi = On W & rng phi c= On W ) by FUNCT_2:def_1, RELAT_1:def_19;
hence  u in Funcs ((On W),(On W)) by FUNCT_2:def_2; ::_thesis: S2[e,u]
take  H ; ::_thesis: ex phi being Ordinal-Sequence of W st
( e = H & u = phi & phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
for va being Function of VAR,(L . a) holds
( Union L,(Union L) ! va |= H iff L . a,va |= H ) ) )
take  phi ; ::_thesis: ( e = H & u = phi & phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
for va being Function of VAR,(L . a) holds
( Union L,(Union L) ! va |= H iff L . a,va |= H ) ) )
thus  ( e = H & u = phi & phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
for va being Function of VAR,(L . a) holds
( Union L,(Union L) ! va |= H iff L . a,va |= H ) ) ) by A4; ::_thesis: verum
end;
consider Phi being Function such that
A5: ( dom Phi = WFF & rng Phi c= Funcs ((On W),(On W)) ) and
A6: for e being set st e in WFF holds
S2[e,Phi . e] from FUNCT_1:sch_5(A3);
reconsider Phi = Phi as Function of WFF,(Funcs ((On W),(On W))) by A5, FUNCT_2:def_1, RELSET_1:4;
 [:omega,omega:] in W by A1, CLASSES2:61;
then  bool [:omega,omega:] in W by CLASSES2:59;
then  ( card WFF c= card (bool [:omega,omega:]) & card (bool [:omega,omega:]) in card W ) by CARD_1:11, CLASSES2:1, ZF_LANG1:134;
then consider phi being Ordinal-Sequence of W such that
A7: ( phi is increasing & phi is continuous ) and
 phi . (0-element_of W) = 0-element_of W and
A8: for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:WFF,{(succ a)}:])) and
A9: for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds
phi . a = sup (phi | a) by Th13, ORDINAL1:12;
take  phi ; ::_thesis: ( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
L . a is_elementary_subsystem_of Union L ) )
thus  ( phi is increasing & phi is continuous ) by A7; ::_thesis: for a being Ordinal of W st phi . a = a & {} <> a holds
L . a is_elementary_subsystem_of Union L
let a be Ordinal of W; ::_thesis: ( phi . a = a & {} <> a implies L . a is_elementary_subsystem_of Union L )
assume that
A10: phi . a = a and
A11: {} <> a ; ::_thesis: L . a is_elementary_subsystem_of Union L
thus  L . a c= Union L by ZF_REFLE:16; :: according to ZFREFLE1:def_3 ::_thesis: for H being ZF-formula
for v being Function of VAR,(L . a) holds
( L . a,v |= H iff Union L,(Union L) ! v |= H )
let H be ZF-formula; ::_thesis: for v being Function of VAR,(L . a) holds
( L . a,v |= H iff Union L,(Union L) ! v |= H )
let va be Function of VAR,(L . a); ::_thesis: ( L . a,va |= H iff Union L,(Union L) ! va |= H )
A12: H in WFF by ZF_LANG:4;
then consider H1 being ZF-formula, xi being Ordinal-Sequence of W such that
A13: H = H1 and
A14: Phi . H = xi and
A15: xi is increasing and
A16: xi is continuous and
A17: for a being Ordinal of W st xi . a = a & {} <> a holds
for va being Function of VAR,(L . a) holds
( Union L,(Union L) ! va |= H1 iff L . a,va |= H1 ) by A6;
defpred S3[ Ordinal] means ( $1 <> {} implies xi . $1 c= phi . $1 );
 a in dom xi by ORDINAL4:34;
then A18: a c= xi . a by A15, ORDINAL4:10;
A19: for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal & ( for b being Ordinal of W st b in a holds
S3[b] ) holds
S3[a]
proof
let a be Ordinal of W; ::_thesis: ( a <> 0-element_of W & a is limit_ordinal & ( for b being Ordinal of W st b in a holds
S3[b] ) implies S3[a] )
assume that
A20: a <> 0-element_of W and
A21: a is limit_ordinal and
A22: for b being Ordinal of W st b in a & b <> {} holds
xi . b c= phi . b and
 a <> {} ; ::_thesis: xi . a c= phi . a
A23: a in dom xi by ORDINAL4:34;
then  xi . a is_limes_of xi | a by A16, A20, A21, ORDINAL2:def_13;
then A24: xi . a = lim (xi | a) by ORDINAL2:def_10;
let A be Ordinal; :: according to ORDINAL1:def_5 ::_thesis: ( not A in xi . a or A in phi . a )
assume A25: A in xi . a ; ::_thesis: A in phi . a
 a c= dom xi by A23, ORDINAL1:def_2;
then A26: dom (xi | a) = a by RELAT_1:62;
 xi | a is increasing by A15, ORDINAL4:15;
then xi . a = sup (xi | a) by A20, A21, A26, A24, ORDINAL4:8
.= sup (rng (xi | a)) ;
then consider B being Ordinal such that
A27: B in rng (xi | a) and
A28: A c= B by A25, ORDINAL2:21;
consider e being set  such that
A29: e in dom (xi | a) and
A30: B = (xi | a) . e by A27, FUNCT_1:def_3;
reconsider e = e as Ordinal by A29;
 a in On W by ZF_REFLE:7;
then  e in On W by A26, A29, ORDINAL1:10;
then reconsider e = e as Ordinal of W by ZF_REFLE:7;
A31: succ e in a by A21, A26, A29, ORDINAL1:28;
 ( e in succ e & succ e in dom xi ) by ORDINAL1:6, ORDINAL4:34;
then A32: xi . e in xi . (succ e) by A15, ORDINAL2:def_12;
 B = xi . e by A29, A30, FUNCT_1:47;
then A33: A in xi . (succ e) by A28, A32, ORDINAL1:12;
 succ e in dom phi by ORDINAL4:34;
then A34: phi . (succ e) in rng (phi | a) by A31, FUNCT_1:50;
phi . a = sup (phi | a) by A9, A20, A21
.= sup (rng (phi | a)) ;
then A35: phi . (succ e) in phi . a by A34, ORDINAL2:19;
 xi . (succ e) c= phi . (succ e) by A22, A31;
hence  A in phi . a by A35, A33, ORDINAL1:10; ::_thesis: verum
end;
A36: for a being Ordinal of W st S3[a] holds
S3[ succ a]
proof
let a be Ordinal of W; ::_thesis: ( S3[a] implies S3[ succ a] )
 succ a in {(succ a)} by TARSKI:def_1;
then A37: [H,(succ a)] in [:WFF,{(succ a)}:] by A12, ZFMISC_1:87;
 succ a in dom xi by ORDINAL4:34;
then  ( [H,(succ a)] in dom (uncurry Phi) & (uncurry Phi) . (H,(succ a)) = xi . (succ a) ) by A5, A12, A14, FUNCT_5:38;
then  xi . (succ a) in (uncurry Phi) .: [:WFF,{(succ a)}:] by A37, FUNCT_1:def_6;
then  xi . (succ a) in {(phi . a)} \/ ((uncurry Phi) .: [:WFF,{(succ a)}:]) by XBOOLE_0:def_3;
then A38: xi . (succ a) in sup ({(phi . a)} \/ ((uncurry Phi) .: [:WFF,{(succ a)}:])) by ORDINAL2:19;
 phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:WFF,{(succ a)}:])) by A8;
hence  ( S3[a] implies S3[ succ a] ) by A38, ORDINAL1:def_2; ::_thesis: verum
end;
A39: S3[ 0-element_of W] ;
 for a being Ordinal of W holds S3[a] from ZF_REFLE:sch_4(A39, A36, A19);
then  xi . a c= a by A10, A11;
then  xi . a = a by A18, XBOOLE_0:def_10;
hence  ( L . a,va |= H iff Union L,(Union L) ! va |= H ) by A11, A13, A17; ::_thesis: verum
end;

theorem Th31: :: ZFREFLE1:31
for W being Universe
for a being Ordinal of W holds Rank a in W
proof
let W be Universe; ::_thesis: for a being Ordinal of W holds Rank a in W
let a be Ordinal of W; ::_thesis: Rank a in W
 ( W = Rank (On W) & a in On W ) by CLASSES2:50, ZF_REFLE:7;
hence  Rank a in W by CLASSES1:36; ::_thesis: verum
end;

theorem Th32: :: ZFREFLE1:32
for W being Universe
for a being Ordinal of W st a <> {} holds
Rank a is non empty Element of W
proof
let W be Universe; ::_thesis: for a being Ordinal of W st a <> {} holds
Rank a is non empty Element of W
let a be Ordinal of W; ::_thesis: ( a <> {} implies Rank a is non empty Element of W )
assume  a <> {} ; ::_thesis: Rank a is non empty Element of W
then  {} in a by ORDINAL3:8;
then reconsider D = Rank a as non empty set by CLASSES1:36;
 D in W by Th31;
hence  Rank a is non empty Element of W ; ::_thesis: verum
end;

theorem Th33: :: ZFREFLE1:33
for W being Universe st omega in W holds
ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & ( for a being Ordinal of W
for M being non empty set st phi . a = a & {} <> a & M = Rank a holds
M is_elementary_subsystem_of W ) )
proof
let W be Universe; ::_thesis: ( omega in W implies ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & ( for a being Ordinal of W
for M being non empty set st phi . a = a & {} <> a & M = Rank a holds
M is_elementary_subsystem_of W ) ) )
deffunc H1( Ordinal, set ) ->  set = Rank $1;
deffunc H2( Ordinal, set ) ->  set = Rank (succ $1);
consider L being T-Sequence such that
A1: ( dom L = On W & ( {} in On W implies L . {} = Rank (1-element_of W) ) ) and
A2: for A being Ordinal st succ A in On W holds
L . (succ A) = H2(A,L . A) and
A3: for A being Ordinal st A in On W & A <> {} & A is limit_ordinal holds
L . A = H1(A,L | A) from ORDINAL2:sch_5();
A4: for a being Ordinal of W st a <> {} & a is limit_ordinal holds
L . a = Rank a
proof
let a be Ordinal of W; ::_thesis: ( a <> {} & a is limit_ordinal implies L . a = Rank a )
 a in On W by ZF_REFLE:7;
hence  ( a <> {} & a is limit_ordinal implies L . a = Rank a ) by A3; ::_thesis: verum
end;
A5: for a being Ordinal of W holds L . (succ a) = Rank (succ a)
proof
let a be Ordinal of W; ::_thesis: L . (succ a) = Rank (succ a)
 succ a in On W by ZF_REFLE:7;
hence  L . (succ a) = Rank (succ a) by A2; ::_thesis: verum
end;
A6: for a being Ordinal of W st a <> {} holds
L . a = Rank a
proof
let a be Ordinal of W; ::_thesis: ( a <> {} implies L . a = Rank a )
A7: now__::_thesis:_(_ex_A_being_Ordinal_st_a_=_succ_A_&_a_<>_{}_implies_L_._a_=_Rank_a_)
A8: a in On W by ZF_REFLE:7;
given A being Ordinal such that A9: a = succ A ; ::_thesis: ( a <> {} implies L . a = Rank a )
 A in a by A9, ORDINAL1:6;
then  A in On W by A8, ORDINAL1:10;
then reconsider A = A as Ordinal of W by ZF_REFLE:7;
 L . (succ A) = Rank (succ A) by A5;
hence  ( a <> {} implies L . a = Rank a ) by A9; ::_thesis: verum
end;
 ( a is limit_ordinal or ex A being Ordinal st a = succ A ) by ORDINAL1:29;
hence  ( a <> {} implies L . a = Rank a ) by A4, A7; ::_thesis: verum
end;
 rng L c= W
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in rng L or e in W )
assume  e in rng L ; ::_thesis: e in W
then consider u being set  such that
A10: u in On W and
A11: e = L . u by A1, FUNCT_1:def_3;
reconsider u = u as Ordinal of W by A10, ZF_REFLE:7;
 ( Rank (1-element_of W) in W & Rank u in W ) by Th31;
hence  e in W by A1, A6, A10, A11; ::_thesis: verum
end;
then reconsider L = L as T-Sequence of W by RELAT_1:def_19;
now__::_thesis:_not_{}_in_rng_L
assume  {} in rng L ; ::_thesis: contradiction
then consider e being set  such that
A12: e in On W and
A13: {} = L . e by A1, FUNCT_1:def_3;
reconsider e = e as Ordinal of W by A12, ZF_REFLE:7;
 ( ( e = {} & 1-element_of W = {{}} ) or e <> {} ) by ORDINAL3:15;
then  ( ( L . e = Rank (1-element_of W) & 1-element_of W <> {} ) or ( e <> {} & L . e = Rank e ) ) by A1, A6, ZF_REFLE:7;
hence  contradiction by A13, Th32; ::_thesis: verum
end;
then reconsider L = L as DOMAIN-Sequence of W by A1, RELAT_1:def_9, ZF_REFLE:def_2;
A14: Union L = W
proof
thus  Union L c= W ; :: according to XBOOLE_0:def_10 ::_thesis: W c= Union L
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in W or e in Union L )
A15: Union L = union (rng L) by CARD_3:def_4;
assume  e in W ; ::_thesis: e in Union L
then A16: e in Rank (On W) by CLASSES2:50;
 On W is limit_ordinal by CLASSES2:51;
then consider A being Ordinal such that
A17: A in On W and
A18: e in Rank A by A16, CLASSES1:31;
reconsider A = A as Ordinal of W by A17, ZF_REFLE:7;
 ( L . A = Rank A & L . A in rng L ) by A1, A6, A17, A18, CLASSES1:29, FUNCT_1:def_3;
then  Rank A c= Union L by A15, ZFMISC_1:74;
hence  e in Union L by A18; ::_thesis: verum
end;
A19: 0-element_of W in On W by ZF_REFLE:7;
A20: for a, b being Ordinal of W st a in b holds
L . a c= L . b
proof
let a, b be Ordinal of W; ::_thesis: ( a in b implies L . a c= L . b )
assume A21: a in b ; ::_thesis: L . a c= L . b
then A22: ( Rank a in Rank b & succ a c= b ) by CLASSES1:36, ORDINAL1:21;
A23: L . b = Rank b by A6, A21;
 ( L . a = Rank a or ( a = 0-element_of W & L . a = Rank (1-element_of W) & 1-element_of W = succ (0-element_of W) ) ) by A1, A19, A6;
hence  L . a c= L . b by A22, A23, CLASSES1:37, ORDINAL1:def_2; ::_thesis: verum
end;
A24: for a being Ordinal of W st a <> {} & a is limit_ordinal holds
L . a = Union (L | a)
proof
let a be Ordinal of W; ::_thesis: ( a <> {} & a is limit_ordinal implies L . a = Union (L | a) )
assume that
A25: a <> {} and
A26: a is limit_ordinal ; ::_thesis: L . a = Union (L | a)
A27: a in On W by ZF_REFLE:7;
A28: L . a = Rank a by A4, A25, A26;
thus  L . a c= Union (L | a) :: according to XBOOLE_0:def_10 ::_thesis: Union (L | a) c= L . a
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in L . a or e in Union (L | a) )
assume  e in L . a ; ::_thesis: e in Union (L | a)
then consider B being Ordinal such that
A29: B in a and
A30: e in Rank B by A25, A26, A28, CLASSES1:31;
 B in On W by A27, A29, ORDINAL1:10;
then reconsider B = B as Ordinal of W by ZF_REFLE:7;
A31: ( succ B in On W & Union (L | a) = union (rng (L | a)) ) by CARD_3:def_4, ZF_REFLE:7;
 L . (succ B) = Rank (succ B) by A5;
then A32: Rank B c= L . (succ B) by CLASSES1:33;
 succ B in a by A26, A29, ORDINAL1:28;
then  L . (succ B) c= Union (L | a) by A1, A31, FUNCT_1:50, ZFMISC_1:74;
then  Rank B c= Union (L | a) by A32, XBOOLE_1:1;
hence  e in Union (L | a) by A30; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in Union (L | a) or e in L . a )
assume  e in Union (L | a) ; ::_thesis: e in L . a
then  e in union (rng (L | a)) by CARD_3:def_4;
then consider X being set  such that
A33: e in X and
A34: X in rng (L | a) by TARSKI:def_4;
consider u being set  such that
A35: u in dom (L | a) and
A36: X = (L | a) . u by A34, FUNCT_1:def_3;
reconsider u = u as Ordinal by A35;
A37: X = L . u by A35, A36, FUNCT_1:47;
A38: dom (L | a) c= a by RELAT_1:58;
then  u in On W by A27, A35, ORDINAL1:10;
then reconsider u = u as Ordinal of W by ZF_REFLE:7;
 L . u c= L . a by A20, A35, A38;
hence  e in L . a by A33, A37; ::_thesis: verum
end;
assume  omega in W ; ::_thesis: ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & ( for a being Ordinal of W
for M being non empty set st phi . a = a & {} <> a & M = Rank a holds
M is_elementary_subsystem_of W ) )
then consider phi being Ordinal-Sequence of W such that
A39: ( phi is increasing & phi is continuous ) and
A40: for a being Ordinal of W st phi . a = a & {} <> a holds
L . a is_elementary_subsystem_of Union L by A20, A24, Th30;
take  phi ; ::_thesis: ( phi is increasing & phi is continuous & ( for a being Ordinal of W
for M being non empty set st phi . a = a & {} <> a & M = Rank a holds
M is_elementary_subsystem_of W ) )
thus  ( phi is increasing & phi is continuous ) by A39; ::_thesis: for a being Ordinal of W
for M being non empty set st phi . a = a & {} <> a & M = Rank a holds
M is_elementary_subsystem_of W
let a be Ordinal of W; ::_thesis: for M being non empty set st phi . a = a & {} <> a & M = Rank a holds
M is_elementary_subsystem_of W
let M be non empty set ; ::_thesis: ( phi . a = a & {} <> a & M = Rank a implies M is_elementary_subsystem_of W )
assume that
A41: phi . a = a and
A42: {} <> a and
A43: M = Rank a ; ::_thesis: M is_elementary_subsystem_of W
 M = L . a by A6, A42, A43;
hence  M is_elementary_subsystem_of W by A40, A14, A41, A42; ::_thesis: verum
end;

theorem Th34: :: ZFREFLE1:34
for W being Universe
for a being Ordinal of W st omega in W holds
ex b being Ordinal of W ex M being non empty set st
( a in b & M = Rank b & M is_elementary_subsystem_of W )
proof
let W be Universe; ::_thesis: for a being Ordinal of W st omega in W holds
ex b being Ordinal of W ex M being non empty set st
( a in b & M = Rank b & M is_elementary_subsystem_of W )
let a be Ordinal of W; ::_thesis: ( omega in W implies ex b being Ordinal of W ex M being non empty set st
( a in b & M = Rank b & M is_elementary_subsystem_of W ) )
assume A1: omega in W ; ::_thesis: ex b being Ordinal of W ex M being non empty set st
( a in b & M = Rank b & M is_elementary_subsystem_of W )
then consider phi being Ordinal-Sequence of W such that
A2: ( phi is increasing & phi is continuous ) and
A3: for a being Ordinal of W
for M being non empty set st phi . a = a & {} <> a & M = Rank a holds
M is_elementary_subsystem_of W by Th33;
consider b being Ordinal of W such that
A4: a in b and
A5: phi . b = b by A1, A2, Th28;
reconsider M = Rank b as non empty set by A4, CLASSES1:36;
take  b ; ::_thesis: ex M being non empty set st
( a in b & M = Rank b & M is_elementary_subsystem_of W )
take  M ; ::_thesis: ( a in b & M = Rank b & M is_elementary_subsystem_of W )
thus  ( a in b & M = Rank b & M is_elementary_subsystem_of W ) by A3, A4, A5; ::_thesis: verum
end;

theorem Th35: :: ZFREFLE1:35
for W being Universe st omega in W holds
ex a being Ordinal of W ex M being non empty set st
( a is_cofinal_with omega & M = Rank a & M is_elementary_subsystem_of W )
proof
let W be Universe; ::_thesis: ( omega in W implies ex a being Ordinal of W ex M being non empty set st
( a is_cofinal_with omega & M = Rank a & M is_elementary_subsystem_of W ) )
set a = the Ordinal of W;
assume A1: omega in W ; ::_thesis: ex a being Ordinal of W ex M being non empty set st
( a is_cofinal_with omega & M = Rank a & M is_elementary_subsystem_of W )
then consider phi being Ordinal-Sequence of W such that
A2: ( phi is increasing & phi is continuous ) and
A3: for a being Ordinal of W
for M being non empty set st phi . a = a & {} <> a & M = Rank a holds
M is_elementary_subsystem_of W by Th33;
consider b being Ordinal of W such that
A4: the Ordinal of W in b and
A5: ( phi . b = b & b is_cofinal_with omega ) by A1, A2, Th29;
reconsider M = Rank b as non empty set by A4, CLASSES1:36;
take  b ; ::_thesis: ex M being non empty set st
( b is_cofinal_with omega & M = Rank b & M is_elementary_subsystem_of W )
take  M ; ::_thesis: ( b is_cofinal_with omega & M = Rank b & M is_elementary_subsystem_of W )
thus  ( b is_cofinal_with omega & M = Rank b & M is_elementary_subsystem_of W ) by A3, A4, A5; ::_thesis: verum
end;

theorem :: ZFREFLE1:36
for W being Universe
for L being DOMAIN-Sequence of W st omega in W & ( for a, b being Ordinal of W st a in b holds
L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds
L . a = Union (L | a) ) holds
ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
L . a <==> Union L ) )
proof
let W be Universe; ::_thesis: for L being DOMAIN-Sequence of W st omega in W & ( for a, b being Ordinal of W st a in b holds
L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds
L . a = Union (L | a) ) holds
ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
L . a <==> Union L ) )
let L be DOMAIN-Sequence of W; ::_thesis: ( omega in W & ( for a, b being Ordinal of W st a in b holds
L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds
L . a = Union (L | a) ) implies ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
L . a <==> Union L ) ) )
assume  ( omega in W & ( for a, b being Ordinal of W st a in b holds
L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds
L . a = Union (L | a) ) ) ; ::_thesis: ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
L . a <==> Union L ) )
then consider phi being Ordinal-Sequence of W such that
A1: ( phi is increasing & phi is continuous ) and
A2: for a being Ordinal of W st phi . a = a & {} <> a holds
L . a is_elementary_subsystem_of Union L by Th30;
take  phi ; ::_thesis: ( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
L . a <==> Union L ) )
thus  ( phi is increasing & phi is continuous ) by A1; ::_thesis: for a being Ordinal of W st phi . a = a & {} <> a holds
L . a <==> Union L
let a be Ordinal of W; ::_thesis: ( phi . a = a & {} <> a implies L . a <==> Union L )
assume  ( phi . a = a & {} <> a ) ; ::_thesis: L . a <==> Union L
hence  L . a <==> Union L by A2, Th9; ::_thesis: verum
end;

theorem :: ZFREFLE1:37
for W being Universe st omega in W holds
ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & ( for a being Ordinal of W
for M being non empty set st phi . a = a & {} <> a & M = Rank a holds
M <==> W ) )
proof
let W be Universe; ::_thesis: ( omega in W implies ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & ( for a being Ordinal of W
for M being non empty set st phi . a = a & {} <> a & M = Rank a holds
M <==> W ) ) )
assume  omega in W ; ::_thesis: ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & ( for a being Ordinal of W
for M being non empty set st phi . a = a & {} <> a & M = Rank a holds
M <==> W ) )
then consider phi being Ordinal-Sequence of W such that
A1: ( phi is increasing & phi is continuous ) and
A2: for a being Ordinal of W
for M being non empty set st phi . a = a & {} <> a & M = Rank a holds
M is_elementary_subsystem_of W by Th33;
take  phi ; ::_thesis: ( phi is increasing & phi is continuous & ( for a being Ordinal of W
for M being non empty set st phi . a = a & {} <> a & M = Rank a holds
M <==> W ) )
thus  ( phi is increasing & phi is continuous ) by A1; ::_thesis: for a being Ordinal of W
for M being non empty set st phi . a = a & {} <> a & M = Rank a holds
M <==> W
let a be Ordinal of W; ::_thesis: for M being non empty set st phi . a = a & {} <> a & M = Rank a holds
M <==> W
let M be non empty set ; ::_thesis: ( phi . a = a & {} <> a & M = Rank a implies M <==> W )
assume  ( phi . a = a & {} <> a & M = Rank a ) ; ::_thesis: M <==> W
hence  M <==> W by A2, Th9; ::_thesis: verum
end;

theorem Th38: :: ZFREFLE1:38
for W being Universe
for a being Ordinal of W st omega in W holds
ex b being Ordinal of W ex M being non empty set st
( a in b & M = Rank b & M <==> W )
proof
let W be Universe; ::_thesis: for a being Ordinal of W st omega in W holds
ex b being Ordinal of W ex M being non empty set st
( a in b & M = Rank b & M <==> W )
let a be Ordinal of W; ::_thesis: ( omega in W implies ex b being Ordinal of W ex M being non empty set st
( a in b & M = Rank b & M <==> W ) )
assume  omega in W ; ::_thesis: ex b being Ordinal of W ex M being non empty set st
( a in b & M = Rank b & M <==> W )
then consider b being Ordinal of W, M being non empty set  such that
A1: ( a in b & M = Rank b & M is_elementary_subsystem_of W ) by Th34;
take  b ; ::_thesis: ex M being non empty set st
( a in b & M = Rank b & M <==> W )
take  M ; ::_thesis: ( a in b & M = Rank b & M <==> W )
thus  ( a in b & M = Rank b & M <==> W ) by A1, Th9; ::_thesis: verum
end;

theorem Th39: :: ZFREFLE1:39
for W being Universe st omega in W holds
ex a being Ordinal of W ex M being non empty set st
( a is_cofinal_with omega & M = Rank a & M <==> W )
proof
let W be Universe; ::_thesis: ( omega in W implies ex a being Ordinal of W ex M being non empty set st
( a is_cofinal_with omega & M = Rank a & M <==> W ) )
assume  omega in W ; ::_thesis: ex a being Ordinal of W ex M being non empty set st
( a is_cofinal_with omega & M = Rank a & M <==> W )
then consider b being Ordinal of W, M being non empty set  such that
A1: ( b is_cofinal_with omega & M = Rank b & M is_elementary_subsystem_of W ) by Th35;
take  b ; ::_thesis: ex M being non empty set st
( b is_cofinal_with omega & M = Rank b & M <==> W )
take  M ; ::_thesis: ( b is_cofinal_with omega & M = Rank b & M <==> W )
thus  ( b is_cofinal_with omega & M = Rank b & M <==> W ) by A1, Th9; ::_thesis: verum
end;

theorem :: ZFREFLE1:40
for W being Universe st omega in W holds
ex a being Ordinal of W ex M being non empty set st
( a is_cofinal_with omega & M = Rank a & M is being_a_model_of_ZF )
proof
let W be Universe; ::_thesis: ( omega in W implies ex a being Ordinal of W ex M being non empty set st
( a is_cofinal_with omega & M = Rank a & M is being_a_model_of_ZF ) )
assume A1: omega in W ; ::_thesis: ex a being Ordinal of W ex M being non empty set st
( a is_cofinal_with omega & M = Rank a & M is being_a_model_of_ZF )
then consider a being Ordinal of W, M being non empty set  such that
A2: ( a is_cofinal_with omega & M = Rank a & M <==> W ) by Th39;
take  a ; ::_thesis: ex M being non empty set st
( a is_cofinal_with omega & M = Rank a & M is being_a_model_of_ZF )
take  M ; ::_thesis: ( a is_cofinal_with omega & M = Rank a & M is being_a_model_of_ZF )
 W is being_a_model_of_ZF by A1, ZF_REFLE:6;
hence  ( a is_cofinal_with omega & M = Rank a & M is being_a_model_of_ZF ) by A2, Th10; ::_thesis: verum
end;

theorem :: ZFREFLE1:41
for X being set
for W being Universe st omega in W & X in W holds
ex M being non empty set st
( X in M & M in W & M is being_a_model_of_ZF )
proof
let X be set ; ::_thesis: for W being Universe st omega in W & X in W holds
ex M being non empty set st
( X in M & M in W & M is being_a_model_of_ZF )
let W be Universe; ::_thesis: ( omega in W & X in W implies ex M being non empty set st
( X in M & M in W & M is being_a_model_of_ZF ) )
assume A1: omega in W ; ::_thesis: ( not X in W or ex M being non empty set st
( X in M & M in W & M is being_a_model_of_ZF ) )
A2: W = Rank (On W) by CLASSES2:50;
assume  X in W ; ::_thesis: ex M being non empty set st
( X in M & M in W & M is being_a_model_of_ZF )
then  the_rank_of X in the_rank_of W by CLASSES1:68;
then  the_rank_of X in On W by A2, CLASSES1:64;
then reconsider a = the_rank_of X as Ordinal of W by ZF_REFLE:7;
consider b being Ordinal of W, M being non empty set  such that
A3: a in b and
A4: M = Rank b and
A5: M <==> W by A1, Th38;
take  M ; ::_thesis: ( X in M & M in W & M is being_a_model_of_ZF )
 X c= Rank a by CLASSES1:def_8;
then A6: X in Rank (succ a) by CLASSES1:32;
 succ a c= b by A3, ORDINAL1:21;
then  Rank (succ a) c= M by A4, CLASSES1:37;
hence  X in M by A6; ::_thesis: ( M in W & M is being_a_model_of_ZF )
 b in On W by ZF_REFLE:7;
hence  M in W by A2, A4, CLASSES1:36; ::_thesis: M is being_a_model_of_ZF
 W is being_a_model_of_ZF by A1, ZF_REFLE:6;
then  W |= ZF-axioms by Th4;
then  M |= ZF-axioms by A5, Th8;
hence  M is being_a_model_of_ZF by A4, Th5; ::_thesis: verum
end;