let W be Universe; :: thesis: for L being DOMAIN-Sequence of 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) ) & ( for a being Ordinal of W holds
( L . a in Union L & L . a is epsilon-transitive ) ) & Union L is closed_wrt_A1-A7 holds
Union L is being_a_model_of_ZF
let L be DOMAIN-Sequence of ; :: 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) ) & ( for a being Ordinal of W holds
( L . a in Union L & L . a is epsilon-transitive ) ) & Union L is closed_wrt_A1-A7 implies Union L is being_a_model_of_ZF )
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 and
A3: for a being Ordinal of W st a <> {} & a is limit_ordinal holds
L . a = Union (L | a) and
A4: for a being Ordinal of W holds
( L . a in Union L & L . a is epsilon-transitive ) and
A5: Union L is closed_wrt_A1-A7 ; :: thesis: Union L is being_a_model_of_ZF
A6: Union L is epsilon-transitive

proof

let X be set ; :: according to ORDINAL1:def 2 :: thesis: ( not X in Union L or X c= Union L )
assume X in Union L ; :: thesis: X c= Union L
then consider u being set such that
A7: ( u in dom L & X in L . u ) by Lm1;
reconsider u = u as Ordinal by A7;
u in On W by A7, ZF_REFLE:def 5;
then reconsider u = u as Ordinal of W by ZF_REFLE:8;
L . u is epsilon-transitive by A4;
then A8: X c= L . u by A7, ORDINAL1:def 2;
let u1 be set ; :: according to TARSKI:def 3 :: thesis: ( not u1 in X or u1 in Union L )
assume u1 in X ; :: thesis: u1 in Union L
then ( u1 in L . u & L . u c= Union L ) by A8, ZF_REFLE:24;
hence u1 in Union L ; :: thesis: verum

end;

then A9: Union L is predicatively_closed by A5, Th5;
for u1, u2 being set st u1 in Union L & u2 in Union L holds
{u1,u2} in Union L by A5, ZF_FUND1:6;
then A10: Union L |= the_axiom_of_pairs by A6, ZFMODEL1:3;
for u being set st u in Union L holds
union u in Union L by A5, ZF_FUND1:2;
then A11: Union L |= the_axiom_of_unions by A6, ZFMODEL1:5;
ex u being set st
( u in Union L & u <> {} & ( for u1 being set st u1 in u holds
ex u2 being set st
( u1 c< u2 & u2 in u ) ) )

proof

deffunc H₁( set , set ) -> set = inf { w where w is Element of W : L . $2 in L . w } ;
consider ksi being Function such that
A12: ( dom ksi = NAT & ksi . 0 = 0-element_of W & ( for i being Nat holds ksi . (i + 1) = H₁(i,ksi . i) ) ) from NAT_1:sch 11();
A13: for i being Element of NAT holds
( ksi . i in On W & ksi . i is Ordinal of W )

proof

defpred S₁[ Element of NAT ] means ( ksi . $1 in On W & ksi . $1 is Ordinal of W );
A14: S₁[ 0 ] by A12, ZF_REFLE:8;

A15: now

let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume S₁[i] ; :: thesis: S₁[i + 1]
then reconsider a = ksi . i as Ordinal of W ;
L . a in Union L by A4;
then consider u being set such that
A16: ( u in dom L & L . a in L . u ) by Lm1;
dom L = On W by ZF_REFLE:def 5;
then reconsider b = u as Ordinal of W by A16, ZF_REFLE:8;
b in { w where w is Element of W : L . a in L . w } by A16;
then A19: inf { w where w is Element of W : L . a in L . w } c= b by ORDINAL2:22;
thus S₁[i + 1] :: thesis: verum

proof

A20: ksi . (i + 1) = inf { w where w is Element of W : L . a in L . w } by A12;
then ksi . (i + 1) in W by A19, CLASSES1:def 1;
hence ksi . (i + 1) in On W by A20, ORDINAL1:def 10; :: thesis: ksi . (i + 1) is Ordinal of W
hence ksi . (i + 1) is Ordinal of W by ZF_REFLE:8; :: thesis: verum

end;

end;

thus for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A14, A15); :: thesis: verum

end;

A21: for i being Element of NAT holds L . (ksi . i) in L . (ksi . (i + 1))

proof

let i be Element of NAT ; :: thesis: L . (ksi . i) in L . (ksi . (i + 1))
A22: ksi . (i + 1) = inf { w where w is Element of W : L . (ksi . i) in L . w } by A12;
reconsider a = ksi . i as Ordinal of W by A13;
L . a in Union L by A4;
then consider b being set such that
A23: ( b in dom L & L . a in L . b ) by Lm1;
b in On W by A23, ZF_REFLE:def 5;
then reconsider b = b as Ordinal of W by ZF_REFLE:8;
b in { w where w is Element of W : L . a in L . w } by A23;
then ksi . (i + 1) in { w where w is Element of W : L . (ksi . i) in L . w } by A22, ORDINAL2:25;
then ex w being Element of W st
( w = ksi . (i + 1) & L . a in L . w ) ;
hence L . (ksi . i) in L . (ksi . (i + 1)) ; :: thesis: verum

end;

A25: for i being Element of NAT holds ksi . i in ksi . (i + 1)

proof

let i be Element of NAT ; :: thesis: ksi . i in ksi . (i + 1)
reconsider a = ksi . i as Ordinal of W by A13;
reconsider b = ksi . (i + 1) as Ordinal of W by A13;
assume not ksi . i in ksi . (i + 1) ; :: thesis: contradiction
then ( b = a or b in a ) by ORDINAL1:24;
then L . b c= L . a by A2;
hence contradiction by A21, ORDINAL1:7; :: thesis: verum

end;

set lambda = sup (rng ksi);
take u = L . (sup (rng ksi)); :: thesis: ( u in Union L & u <> {} & ( for u1 being set st u1 in u holds
ex u2 being set st
( u1 c< u2 & u2 in u ) ) )
sup (rng ksi) in On W

proof

A26: rng ksi c= W

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in rng ksi or a in W )
assume a in rng ksi ; :: thesis: a in W
then consider i being set such that
A27: ( i in dom ksi & a = ksi . i ) by FUNCT_1:def 5;
reconsider i = i as Element of NAT by A12, A27;
ksi . i in On W by A13;
hence a in W by A27, ORDINAL1:def 10; :: thesis: verum

end;

( card (rng ksi) c= card NAT & card NAT = card omega & card omega in card W ) by A1, A12, CARD_1:28, CLASSES2:1;
then card (rng ksi) in card W by ORDINAL1:22;
then rng ksi in W by A26, CLASSES1:2;
then sup (rng ksi) in W by ZF_REFLE:28;
hence sup (rng ksi) in On W by ORDINAL1:def 10; :: thesis: verum

end;

then reconsider l = sup (rng ksi) as Ordinal of W by ZF_REFLE:8;
( L . l in Union L & L . l <> {} ) by A4;
hence ( u in Union L & u <> {} ) ; :: thesis: for u1 being set st u1 in u holds
ex u2 being set st
( u1 c< u2 & u2 in u )
A28: l is limit_ordinal

proof

A29: union l c= l by ORDINAL2:5;
l c= union l

proof

let u1 be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not u1 in l or u1 in union l )
assume u1 in l ; :: thesis: u1 in union l
then consider u2 being Ordinal such that
A30: ( u2 in rng ksi & u1 c= u2 ) by ORDINAL2:29;
consider i being set such that
A31: ( i in dom ksi & u2 = ksi . i ) by A30, FUNCT_1:def 5;
reconsider i = i as Element of NAT by A12, A31;
reconsider u3 = ksi . (i + 1) as Ordinal of W by A13;
( u3 in rng ksi & u2 in u3 ) by A12, A25, A31, FUNCT_1:def 5;
then ( u3 in l & u1 in u3 ) by A30, ORDINAL1:22, ORDINAL2:27;
hence u1 in union l by TARSKI:def 4; :: thesis: verum

end;

then l = union l by A29, XBOOLE_0:def 10;
hence l is limit_ordinal by ORDINAL1:def 6; :: thesis: verum

end;

A32: union { (L . (ksi . n)) where n is Element of NAT : verum } = L . l

proof

set A = { (L . (ksi . n)) where n is Element of NAT : verum } ;
thus union { (L . (ksi . n)) where n is Element of NAT : verum } c= L . l :: according to XBOOLE_0:def 10 :: thesis: L . l c= union { (L . (ksi . n)) where n is Element of NAT : verum }

proof

let u1 be set ; :: according to TARSKI:def 3 :: thesis: ( not u1 in union { (L . (ksi . n)) where n is Element of NAT : verum } or u1 in L . l )
assume u1 in union { (L . (ksi . n)) where n is Element of NAT : verum } ; :: thesis: u1 in L . l
then consider X being set such that
A33: ( u1 in X & X in { (L . (ksi . n)) where n is Element of NAT : verum } ) by TARSKI:def 4;
consider n being Element of NAT such that
A34: X = L . (ksi . n) by A33;
reconsider a = ksi . n as Ordinal of W by A13;
a in rng ksi by A12, FUNCT_1:def 5;
then L . a c= L . l by A2, ORDINAL2:27;
hence u1 in L . l by A33, A34; :: thesis: verum

end;

let u1 be set ; :: according to TARSKI:def 3 :: thesis: ( not u1 in L . l or u1 in union { (L . (ksi . n)) where n is Element of NAT : verum } )
assume A35: u1 in L . l ; :: thesis: u1 in union { (L . (ksi . n)) where n is Element of NAT : verum }
0-element_of W in rng ksi by A12, FUNCT_1:def 5;
then l <> {} by ORDINAL2:27;
then L . l = Union (L | l) by A3, A28;
then consider u2 being set such that
A36: ( u2 in dom (L | l) & u1 in (L | l) . u2 ) by A35, Lm1;
A37: ( u2 in (dom L) /\ l & u1 in L . u2 ) by A36, FUNCT_1:70, RELAT_1:90;
then A38: ( u2 in dom L & u2 in l ) by XBOOLE_0:def 4;
then u2 in On W by ZF_REFLE:def 5;
then reconsider u2 = u2 as Ordinal of W by ZF_REFLE:8;
consider b being Ordinal such that
A39: ( b in rng ksi & u2 c= b ) by A38, ORDINAL2:29;
consider i being set such that
A40: ( i in dom ksi & b = ksi . i ) by A39, FUNCT_1:def 5;
reconsider i = i as Element of NAT by A12, A40;
b = ksi . i by A40;
then reconsider b = b as Ordinal of W by A13;
( u2 c< b iff ( u2 c= b & u2 <> b ) ) by XBOOLE_0:def 8;
then L . u2 c= L . b by A2, A39, ORDINAL1:21;
then ( u1 in L . (ksi . i) & L . (ksi . i) in { (L . (ksi . n)) where n is Element of NAT : verum } ) by A37, A40;
hence u1 in union { (L . (ksi . n)) where n is Element of NAT : verum } by TARSKI:def 4; :: thesis: verum

end;

let u1 be set ; :: thesis: ( u1 in u implies ex u2 being set st
( u1 c< u2 & u2 in u ) )
assume u1 in u ; :: thesis: ex u2 being set st
( u1 c< u2 & u2 in u )
then consider u2 being set such that
A41: ( u1 in u2 & u2 in { (L . (ksi . n)) where n is Element of NAT : verum } ) by A32, TARSKI:def 4;
take u2 ; :: thesis: ( u1 c< u2 & u2 in u )
consider i being Element of NAT such that
A42: u2 = L . (ksi . i) by A41;
reconsider a = ksi . i as Ordinal of W by A13;
L . a is epsilon-transitive by A4;
then A43: u1 c= u2 by A41, A42, ORDINAL1:def 2;
u1 <> u2 by A41;
hence u1 c< u2 by A43, XBOOLE_0:def 8; :: thesis: u2 in u
thus u2 in u :: thesis: verum

proof

( L . (ksi . i) in L . (ksi . (i + 1)) & L . (ksi . (i + 1)) in { (L . (ksi . n)) where n is Element of NAT : verum } ) by A21;
hence u2 in u by A32, A42, TARSKI:def 4; :: thesis: verum

end;

end;

then A44: Union L |= the_axiom_of_infinity by A6, ZFMODEL1:7;
A45: Union L |= the_axiom_of_power_sets by A2, A4, A9, Th2;
for H being ZF-formula st {(x. 0 ),(x. 1),(x. 2)} misses Free H holds
Union L |= the_axiom_of_substitution_for H by A1, A2, A3, A4, A9, Th3;
hence Union L is being_a_model_of_ZF by A6, A10, A11, A44, A45, ZF_MODEL:def 12; :: thesis: verum