let W be Universe; :: thesis: for L being DOMAIN-Sequence of st ( for a, b being Ordinal of W st a in b holds
L . a c= L . b ) & ( for a being Ordinal of W holds
( L . a in Union L & L . a is epsilon-transitive ) ) & Union L is predicatively_closed holds
Union L |= the_axiom_of_power_sets
let L be DOMAIN-Sequence of ; :: thesis: ( ( for a, b being Ordinal of W st a in b holds
L . a c= L . b ) & ( for a being Ordinal of W holds
( L . a in Union L & L . a is epsilon-transitive ) ) & Union L is predicatively_closed implies Union L |= the_axiom_of_power_sets )
assume that
A1: for a, b being Ordinal of W st a in b holds
L . a c= L . b and
A2: for a being Ordinal of W holds
( L . a in Union L & L . a is epsilon-transitive ) and
A3: Union L is predicatively_closed ; :: thesis: Union L |= the_axiom_of_power_sets
A4: 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
A5: ( u in dom L & X in L . u ) by Lm1;
reconsider u = u as Ordinal by A5;
u in On W by A5, ZF_REFLE:def 5;
then reconsider u = u as Ordinal of W by ZF_REFLE:8;
L . u is epsilon-transitive by A2;
then A6: X c= L . u by A5, 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 A6, ZF_REFLE:24;
hence u1 in Union L ; :: thesis: verum

end;

set M = Union L;
A7: for X being set
for a being Ordinal of W st X in L . a holds
(L . a) /\ (bool X) in Union L

proof

let X be set ; :: thesis: for a being Ordinal of W st X in L . a holds
(L . a) /\ (bool X) in Union L
let a be Ordinal of W; :: thesis: ( X in L . a implies (L . a) /\ (bool X) in Union L )
assume X in L . a ; :: thesis: (L . a) /\ (bool X) in Union L
then reconsider e = X as Element of L . a ;
consider f being Function of VAR ,(L . a);
L . a in Union L by A2;
then ( Section (All (x. 2),(((x. 2) 'in' (x. 0 )) => ((x. 2) 'in' (x. 1)))),(f / (x. 1),e) in Union L & L . a is epsilon-transitive ) by A2, A3, Def2;
hence (L . a) /\ (bool X) in Union L by Th1; :: thesis: verum

end;

now

let X be set ; :: thesis: ( X in Union L implies (Union L) /\ (bool X) in Union L )
assume A8: X in Union L ; :: thesis: (Union L) /\ (bool X) in Union L
A9: X in bool X by ZFMISC_1:def 1;
then A10: X in (Union L) /\ (bool X) by A8, XBOOLE_0:def 4;
reconsider D = (Union L) /\ (bool X) as non empty set by A8, A9, XBOOLE_0:def 4;
defpred S₁[ set , set ] means $1 in L . $2;
A11: for d being Element of D ex a being Ordinal of W st S₁[d,a]

proof

let d be Element of D; :: thesis: ex a being Ordinal of W st S₁[d,a]
d in Union L by XBOOLE_0:def 4;
then consider u2 being set such that
A12: ( u2 in dom L & d in L . u2 ) by Lm1;
u2 in On W by A12, ZF_REFLE:def 5;
then reconsider u2 = u2 as Ordinal of W by ZF_REFLE:8;
take u2 ; :: thesis: S₁[d,u2]
thus S₁[d,u2] by A12; :: thesis: verum

end;

consider f being Function such that
A13: ( dom f = D & ( for d being Element of D ex a being Ordinal of W st
( a = f . d & S₁[d,a] & ( for b being Ordinal of W st S₁[d,b] holds
a c= b ) ) ) ) from ZF_REFLE:sch 1(A11);
A14: rng f c= W

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in rng f or u in W )
assume u in rng f ; :: thesis: u in W
then consider u1 being set such that
A15: ( u1 in D & u = f . u1 ) by A13, FUNCT_1:def 5;
reconsider u1 = u1 as Element of D by A15;
ex a being Ordinal of W st
( a = f . u1 & u1 in L . a & ( for b being Ordinal of W st u1 in L . b holds
a c= b ) ) by A13;
hence u in W by A15; :: thesis: verum

end;

( bool X in W & (Union L) /\ (bool X) c= bool X ) by A8, CLASSES2:65, XBOOLE_1:17;
then ( D in W & rng f = f .: (dom f) ) by CLASSES1:def 1, RELAT_1:146;
then ( card D in card W & card (rng f) c= card (dom f) ) by CARD_2:3, CLASSES2:1;
then ( card (rng f) in card W & W is Tarski ) by A13, ORDINAL1:22;
then rng f in W by A14, CLASSES1:2;
then sup (rng f) in W by ZF_REFLE:28;
then reconsider a = sup (rng f) as Ordinal of W ;
A16: D c= L . a

proof

let u2 be set ; :: according to TARSKI:def 3 :: thesis: ( not u2 in D or u2 in L . a )
assume u2 in D ; :: thesis: u2 in L . a
then reconsider d = u2 as Element of D ;
consider c being Ordinal of W such that
A17: ( c = f . d & d in L . c & ( for b being Ordinal of W st d in L . b holds
c c= b ) ) by A13;
c in rng f by A13, A17, FUNCT_1:def 5;
then L . c c= L . a by A1, ORDINAL2:27;
hence u2 in L . a by A17; :: thesis: verum

end;

then ( D /\ (bool X) = (Union L) /\ ((bool X) /\ (bool X)) & (bool X) /\ (bool X) = bool X & D /\ (bool X) c= (L . a) /\ (bool X) & L . a c= Union L ) by XBOOLE_1:16, XBOOLE_1:26, ZF_REFLE:24;
then ( D c= (L . a) /\ (bool X) & (L . a) /\ (bool X) c= D ) by XBOOLE_1:26;
then D = (L . a) /\ (bool X) by XBOOLE_0:def 10;
hence (Union L) /\ (bool X) in Union L by A7, A10, A16; :: thesis: verum

end;

hence Union L |= the_axiom_of_power_sets by A4, ZFMODEL1:9; :: thesis: verum