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) ) & ( 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 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) ) & ( 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 and
A8: X in L . u by Lm1;
reconsider u = u as Ordinal by A7;
u in On W by A7, ZF_REFLE:def 2;
then reconsider u = u as Ordinal of W by ZF_REFLE:7;
L . u is epsilon-transitive by A4;
then A9: X c= L . u by A8;
let u1 be object ; :: according to TARSKI:def 3 :: thesis: ( not u1 in X or u1 in Union L )
A10: L . u c= Union L by ZF_REFLE:16;
assume u1 in X ; :: thesis: u1 in Union L
then u1 in L . u by A9;
hence u1 in Union L by A10; :: thesis: verum
end;
then Union L is predicatively_closed by A5, Th5;
then A11: ( Union L |= the_axiom_of_power_sets & ( 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, Th2, Th3;
for u being set st u in Union L holds
union u in Union L by A5, ZF_FUND1:2;
then A12: Union L |= the_axiom_of_unions by A6, ZFMODEL1:5;
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 A13: Union L |= the_axiom_of_pairs by A6, ZFMODEL1:3;
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
A14: card omega in card W by A1, CLASSES2:1;
deffunc H1( set , set ) -> set = inf { w where w is Element of W : L . $2 in L . w } ;
consider ksi being Function such that
A15: ( dom ksi = NAT & ksi . 0 = 0-element_of W & ( for i being Nat holds ksi . (i + 1) = H1(i,ksi . i) ) ) from NAT_1:sch 11();
 card (rng ksi) c= card NAT by A15, CARD_1:12;
then A16: card (rng ksi) in card W by A14, ORDINAL1:12;
set lambda = sup (rng ksi);
A17: for i being Nat holds
( ksi . i in On W & ksi . i is Ordinal of W )
proof
defpred S1[ Nat] means ( ksi . $1 in On W & ksi . $1 is Ordinal of W );
A18: now :: thesis: for i being Nat st S1[i] holds
S1[i + 1]
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume S1[i] ; :: thesis: S1[i + 1]
then reconsider a = ksi . i as Ordinal of W ;
A19: ksi . (i + 1) = inf { w where w is Element of W : L . a in L . w } by A15;
consider u being set such that
A20: u in dom L and
A21: L . a in L . u by A4, Lm1;
dom L = On W by ZF_REFLE:def 2;
then reconsider b = u as Ordinal of W by A20, ZF_REFLE:7;
b in { w where w is Element of W : L . a in L . w } by A21;
then inf { w where w is Element of W : L . a in L . w } c= b by ORDINAL2:14;
then ksi . (i + 1) in W by A19, CLASSES1:def 1;
hence S1[i + 1] by A19, ORDINAL1:def 9; :: thesis: verum
end;
A22: S1[ 0 ] by A15, ZF_REFLE:7;
thus for i being Nat holds S1[i] from NAT_1:sch 2(A22, A18); :: thesis: verum
end;
rng ksi c= W
proof
let a be object ; :: 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 object such that
A23: i in dom ksi and
A24: a = ksi . i by FUNCT_1:def 3;
reconsider i = i as Element of NAT by A15, A23;
ksi . i in On W by A17;
hence a in W by A24, ORDINAL1:def 9; :: thesis: verum
end;
then rng ksi in W by A16, CLASSES1:1;
then reconsider l = sup (rng ksi) as Ordinal of W by ZF_REFLE:19;
A25: 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))
reconsider a = ksi . i as Ordinal of W by A17;
consider b being set such that
A26: b in dom L and
A27: L . a in L . b by A4, Lm1;
b in On W by A26, ZF_REFLE:def 2;
then reconsider b = b as Ordinal of W by ZF_REFLE:7;
A28: b in { w where w is Element of W : L . a in L . w } by A27;
ksi . (i + 1) = inf { w where w is Element of W : L . (ksi . i) in L . w } by A15;
then ksi . (i + 1) in { w where w is Element of W : L . (ksi . i) in L . w } by A28, ORDINAL2:17;
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;
A29: 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 b = ksi . (i + 1) as Ordinal of W by A17;
reconsider a = ksi . i as Ordinal of W by A17;
assume not ksi . i in ksi . (i + 1) ; :: thesis: contradiction
then ( b = a or b in a ) by ORDINAL1:14;
then L . b c= L . a by A2;
hence contradiction by A25, ORDINAL1:5; :: thesis: verum
end;
A30: 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
A31: u2 in rng ksi and
A32: u1 c= u2 by ORDINAL2:21;
consider i being object such that
A33: i in dom ksi and
A34: u2 = ksi . i by A31, FUNCT_1:def 3;
reconsider i = i as Element of NAT by A15, A33;
reconsider u3 = ksi . (i + 1) as Ordinal of W by A17;
u3 in rng ksi by A15, FUNCT_1:def 3;
then A35: u3 in l by ORDINAL2:19;
u1 in u3 by A29, A32, A34, ORDINAL1:12;
hence u1 in union l by A35, TARSKI:def 4; :: thesis: verum
end;
union l c= l by ORDINAL2:5;
then l = union l by A30;
then A36: l is limit_ordinal ;
A37: 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 object ; :: 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
A38: u1 in X and
A39: X in { (L . (ksi . n)) where n is Element of NAT : verum } by TARSKI:def 4;
consider n being Element of NAT such that
A40: X = L . (ksi . n) by A39;
reconsider a = ksi . n as Ordinal of W by A17;
a in rng ksi by A15, FUNCT_1:def 3;
then L . a c= L . l by A2, ORDINAL2:19;
hence u1 in L . l by A38, A40; :: thesis: verum
end;
0-element_of W in rng ksi by A15, FUNCT_1:def 3;
then l <> {} by ORDINAL2:19;
then A41: L . l = Union (L | l) by A3, A36;
let u1 be object ; :: 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 u1 in L . l ; :: thesis: u1 in union { (L . (ksi . n)) where n is Element of NAT : verum }
then consider u2 being set such that
A42: u2 in dom (L | l) and
A43: u1 in (L | l) . u2 by A41, Lm1;
A44: u1 in L . u2 by A42, A43, FUNCT_1:47;
A45: u2 in (dom L) /\ l by A42, RELAT_1:61;
then A46: u2 in l by XBOOLE_0:def 4;
u2 in dom L by A45, XBOOLE_0:def 4;
then u2 in On W by ZF_REFLE:def 2;
then reconsider u2 = u2 as Ordinal of W by ZF_REFLE:7;
consider b being Ordinal such that
A47: b in rng ksi and
A48: u2 c= b by A46, ORDINAL2:21;
consider i being object such that
A49: i in dom ksi and
A50: b = ksi . i by A47, FUNCT_1:def 3;
reconsider i = i as Element of NAT by A15, A49;
b = ksi . i by A50;
then reconsider b = b as Ordinal of W by A17;
( u2 c< b iff ( u2 c= b & u2 <> b ) ) ;
then A51: L . u2 c= L . b by A2, A48, ORDINAL1:11;
L . (ksi . i) in { (L . (ksi . n)) where n is Element of NAT : verum } ;
hence u1 in union { (L . (ksi . n)) where n is Element of NAT : verum } by A44, A50, A51, TARSKI:def 4; :: thesis: verum
end;
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 ) ) )
L . l in Union 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 )
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
A52: ( u1 in u2 & u2 in { (L . (ksi . n)) where n is Element of NAT : verum } ) by A37, TARSKI:def 4;
take u2 ; :: thesis: ( u1 c< u2 & u2 in u )
consider i being Element of NAT such that
A53: u2 = L . (ksi . i) by A52;
A54: u1 <> u2 by A52;
reconsider a = ksi . i as Ordinal of W by A17;
L . a is epsilon-transitive by A4;
then u1 c= u2 by A52, A53;
hence u1 c< u2 by A54; :: thesis: u2 in u
A55: L . (ksi . (i + 1)) in { (L . (ksi . n)) where n is Element of NAT : verum } ;
L . (ksi . i) in L . (ksi . (i + 1)) by A25;
hence u2 in u by A37, A53, A55, TARSKI:def 4; :: thesis: verum
end;
then Union L |= the_axiom_of_infinity by A6, ZFMODEL1:7;
hence Union L is being_a_model_of_ZF by A6, A13, A12, A11, ZF_MODEL:def 12; :: thesis: verum