let E be non empty set ; :: thesis: ( E is epsilon-transitive implies ( E |= the_axiom_of_power_sets iff for u being Element of E holds E /\ (bool u) in E ) )
assume A1: for X being set st X in E holds
X c= E ; :: according to ORDINAL1:def 2 :: thesis: ( E |= the_axiom_of_power_sets iff for u being Element of E holds E /\ (bool u) in E )
thus ( E |= the_axiom_of_power_sets implies for u being Element of E holds E /\ (bool u) in E ) :: thesis: ( ( for u being Element of E holds E /\ (bool u) in E ) implies E |= the_axiom_of_power_sets )

proof

consider f0 being Function of VAR ,E;
assume A2: E |= the_axiom_of_power_sets ; :: thesis: for u being Element of E holds E /\ (bool u) in E
let u be Element of E; :: thesis: E /\ (bool u) in E
set f = f0 +* (x. 0 ),u;
E |= Ex (x. 1),(All (x. 2),(((x. 2) 'in' (x. 1)) <=> (All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 )))))) by A2, ZF_MODEL:25;
then E,f0 +* (x. 0 ),u |= Ex (x. 1),(All (x. 2),(((x. 2) 'in' (x. 1)) <=> (All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 )))))) by ZF_MODEL:def 5;
then consider g being Function of VAR ,E such that
A3: for x being Variable st g . x <> (f0 +* (x. 0 ),u) . x holds
x. 1 = x and
A4: E,g |= All (x. 2),(((x. 2) 'in' (x. 1)) <=> (All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 ))))) by ZF_MODEL:20;
A5: (f0 +* (x. 0 ),u) . (x. 0 ) = u by FUNCT_7:130;
g . (x. 1) = E /\ (bool u)

proof

thus for a being set st a in g . (x. 1) holds
a in E /\ (bool u) :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: E /\ (bool u) c= g . (x. 1)

proof

let a be set ; :: thesis: ( a in g . (x. 1) implies a in E /\ (bool u) )
assume A6: a in g . (x. 1) ; :: thesis: a in E /\ (bool u)
g . (x. 1) c= E by A1;
then reconsider a9 = a as Element of E by A6;
set h = g +* (x. 2),a9;
A7: (g +* (x. 2),a9) . (x. 2) = a9 by FUNCT_7:130;
for x being Variable st (g +* (x. 2),a9) . x <> g . x holds
x. 2 = x by FUNCT_7:34;
then A8: E,g +* (x. 2),a9 |= ((x. 2) 'in' (x. 1)) <=> (All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 )))) by A4, ZF_MODEL:16;
(g +* (x. 2),a9) . (x. 1) = g . (x. 1) by FUNCT_7:34;
then E,g +* (x. 2),a9 |= (x. 2) 'in' (x. 1) by A6, A7, ZF_MODEL:13;
then A9: E,g +* (x. 2),a9 |= All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 ))) by A8, ZF_MODEL:19;
a9 c= u

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in a9 or b in u )
assume A10: b in a9 ; :: thesis: b in u
a9 c= E by A1;
then reconsider b9 = b as Element of E by A10;
set m = (g +* (x. 2),a9) +* (x. 3),b9;
A11: ((g +* (x. 2),a9) +* (x. 3),b9) . (x. 3) = b9 by FUNCT_7:130;
for x being Variable st ((g +* (x. 2),a9) +* (x. 3),b9) . x <> (g +* (x. 2),a9) . x holds
x. 3 = x by FUNCT_7:34;
then A12: E,(g +* (x. 2),a9) +* (x. 3),b9 |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 )) by A9, ZF_MODEL:16;
((g +* (x. 2),a9) +* (x. 3),b9) . (x. 2) = (g +* (x. 2),a9) . (x. 2) by FUNCT_7:34;
then E,(g +* (x. 2),a9) +* (x. 3),b9 |= (x. 3) 'in' (x. 2) by A7, A10, A11, ZF_MODEL:13;
then A13: E,(g +* (x. 2),a9) +* (x. 3),b9 |= (x. 3) 'in' (x. 0 ) by A12, ZF_MODEL:18;
A14: ( ((g +* (x. 2),a9) +* (x. 3),b9) . (x. 0 ) = (g +* (x. 2),a9) . (x. 0 ) & (g +* (x. 2),a9) . (x. 0 ) = g . (x. 0 ) ) by FUNCT_7:34;
g . (x. 0 ) = (f0 +* (x. 0 ),u) . (x. 0 ) by A3;
hence b in u by A5, A11, A13, A14, ZF_MODEL:13; :: thesis: verum

end;

hence a in E /\ (bool u) by XBOOLE_0:def 4; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in E /\ (bool u) or a in g . (x. 1) )
assume A15: a in E /\ (bool u) ; :: thesis: a in g . (x. 1)
then A16: a in bool u by XBOOLE_0:def 4;
reconsider a = a as Element of E by A15, XBOOLE_0:def 4;
set h = g +* (x. 2),a;
A17: (g +* (x. 2),a) . (x. 2) = a by FUNCT_7:130;

now

let m be Function of VAR ,E; :: thesis: ( ( for x being Variable st m . x <> (g +* (x. 2),a) . x holds
x. 3 = x ) implies E,m |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 )) )
assume A18: for x being Variable st m . x <> (g +* (x. 2),a) . x holds
x. 3 = x ; :: thesis: E,m |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 ))

now

assume E,m |= (x. 3) 'in' (x. 2) ; :: thesis: E,m |= (x. 3) 'in' (x. 0 )
then A19: m . (x. 3) in m . (x. 2) by ZF_MODEL:13;
A20: ( (g +* (x. 2),a) . (x. 0 ) = g . (x. 0 ) & g . (x. 0 ) = (f0 +* (x. 0 ),u) . (x. 0 ) ) by A3, FUNCT_7:34;
( m . (x. 2) = (g +* (x. 2),a) . (x. 2) & m . (x. 0 ) = (g +* (x. 2),a) . (x. 0 ) ) by A18;
hence E,m |= (x. 3) 'in' (x. 0 ) by A5, A16, A17, A19, A20, ZF_MODEL:13; :: thesis: verum

end;

hence E,m |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 )) by ZF_MODEL:18; :: thesis: verum

end;

then A21: E,g +* (x. 2),a |= All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 ))) by ZF_MODEL:16;
A22: (g +* (x. 2),a) . (x. 1) = g . (x. 1) by FUNCT_7:34;
for x being Variable st (g +* (x. 2),a) . x <> g . x holds
x. 2 = x by FUNCT_7:34;
then E,g +* (x. 2),a |= ((x. 2) 'in' (x. 1)) <=> (All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 )))) by A4, ZF_MODEL:16;
then E,g +* (x. 2),a |= (x. 2) 'in' (x. 1) by A21, ZF_MODEL:19;
hence a in g . (x. 1) by A17, A22, ZF_MODEL:13; :: thesis: verum

end;

hence E /\ (bool u) in E ; :: thesis: verum

end;

assume A23: for u being Element of E holds E /\ (bool u) in E ; :: thesis: E |= the_axiom_of_power_sets
E |= Ex (x. 1),(All (x. 2),(((x. 2) 'in' (x. 1)) <=> (All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 ))))))

proof

let f be Function of VAR ,E; :: according to ZF_MODEL:def 5 :: thesis: E,f |= Ex (x. 1),(All (x. 2),(((x. 2) 'in' (x. 1)) <=> (All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 ))))))
reconsider v = E /\ (bool (f . (x. 0 ))) as Element of E by A23;
set g = f +* (x. 1),v;
A24: (f +* (x. 1),v) . (x. 1) = v by FUNCT_7:130;

now

let h be Function of VAR ,E; :: thesis: ( ( for x being Variable st h . x <> (f +* (x. 1),v) . x holds
x. 2 = x ) implies E,h |= ((x. 2) 'in' (x. 1)) <=> (All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 )))) )
assume A25: for x being Variable st h . x <> (f +* (x. 1),v) . x holds
x. 2 = x ; :: thesis: E,h |= ((x. 2) 'in' (x. 1)) <=> (All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 ))))

now

thus ( E,h |= (x. 2) 'in' (x. 1) implies E,h |= All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 ))) ) :: thesis: ( E,h |= All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 ))) implies E,h |= (x. 2) 'in' (x. 1) )

proof

assume E,h |= (x. 2) 'in' (x. 1) ; :: thesis: E,h |= All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 )))
then A26: h . (x. 2) in h . (x. 1) by ZF_MODEL:13;
h . (x. 1) = v by A24, A25;
then A27: h . (x. 2) in bool (f . (x. 0 )) by A26, XBOOLE_0:def 4;

now

let m be Function of VAR ,E; :: thesis: ( ( for x being Variable st m . x <> h . x holds
x. 3 = x ) implies E,m |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 )) )
assume A28: for x being Variable st m . x <> h . x holds
x. 3 = x ; :: thesis: E,m |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 ))

now

assume E,m |= (x. 3) 'in' (x. 2) ; :: thesis: E,m |= (x. 3) 'in' (x. 0 )
then A29: m . (x. 3) in m . (x. 2) by ZF_MODEL:13;
A30: ( m . (x. 2) = h . (x. 2) & f . (x. 0 ) = (f +* (x. 1),v) . (x. 0 ) ) by A28, FUNCT_7:34;
( (f +* (x. 1),v) . (x. 0 ) = h . (x. 0 ) & h . (x. 0 ) = m . (x. 0 ) ) by A25, A28;
hence E,m |= (x. 3) 'in' (x. 0 ) by A27, A29, A30, ZF_MODEL:13; :: thesis: verum

end;

hence E,m |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 )) by ZF_MODEL:18; :: thesis: verum

end;

hence E,h |= All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 ))) by ZF_MODEL:16; :: thesis: verum

end;

assume A31: E,h |= All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 ))) ; :: thesis: E,h |= (x. 2) 'in' (x. 1)
A32: h . (x. 2) c= f . (x. 0 )

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in h . (x. 2) or a in f . (x. 0 ) )
assume A33: a in h . (x. 2) ; :: thesis: a in f . (x. 0 )
h . (x. 2) c= E by A1;
then reconsider a9 = a as Element of E by A33;
set m = h +* (x. 3),a9;
A34: (h +* (x. 3),a9) . (x. 3) = a9 by FUNCT_7:130;
for x being Variable st (h +* (x. 3),a9) . x <> h . x holds
x. 3 = x by FUNCT_7:34;
then A35: E,h +* (x. 3),a9 |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 )) by A31, ZF_MODEL:16;
(h +* (x. 3),a9) . (x. 2) = h . (x. 2) by FUNCT_7:34;
then E,h +* (x. 3),a9 |= (x. 3) 'in' (x. 2) by A33, A34, ZF_MODEL:13;
then E,h +* (x. 3),a9 |= (x. 3) 'in' (x. 0 ) by A35, ZF_MODEL:18;
then A36: (h +* (x. 3),a9) . (x. 3) in (h +* (x. 3),a9) . (x. 0 ) by ZF_MODEL:13;
( (h +* (x. 3),a9) . (x. 0 ) = h . (x. 0 ) & (f +* (x. 1),v) . (x. 0 ) = f . (x. 0 ) ) by FUNCT_7:34;
hence a in f . (x. 0 ) by A25, A34, A36; :: thesis: verum

end;

h . (x. 1) = (f +* (x. 1),v) . (x. 1) by A25;
then h . (x. 2) in h . (x. 1) by A24, A32, XBOOLE_0:def 4;
hence E,h |= (x. 2) 'in' (x. 1) by ZF_MODEL:13; :: thesis: verum

end;

hence E,h |= ((x. 2) 'in' (x. 1)) <=> (All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 )))) by ZF_MODEL:19; :: thesis: verum

end;

then A37: E,f +* (x. 1),v |= All (x. 2),(((x. 2) 'in' (x. 1)) <=> (All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 ))))) by ZF_MODEL:16;
for x being Variable st (f +* (x. 1),v) . x <> f . x holds
x. 1 = x by FUNCT_7:34;
hence E,f |= Ex (x. 1),(All (x. 2),(((x. 2) 'in' (x. 1)) <=> (All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 )))))) by A37, ZF_MODEL:20; :: thesis: verum

end;

hence E |= the_axiom_of_power_sets by ZF_MODEL:25; :: thesis: verum