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

set f0 = the 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 = the Function of VAR,E +* ((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:23;
then E, the Function of VAR,E +* ((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))))))))) ;
then consider g being Function of VAR,E such that
A3: for x being Variable st g . x <> ( the Function of VAR,E +* ((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: ( the Function of VAR,E +* ((x. 0),u)) . (x. 0) = u by FUNCT_7:128;
g . (x. 1) = E /\ (bool u)

proof

thus for a being object 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 object ; :: 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:128;
for x being Variable st (g +* ((x. 2),a9)) . x <> g . x holds
x. 2 = x by FUNCT_7:32;
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:32;
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 object ; :: 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:128;
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:32;
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:32;
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:32;
g . (x. 0) = ( the Function of VAR,E +* ((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 object ; :: 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:128;

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

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 :: thesis: ( E,m |= (x. 3) 'in' (x. 2) implies E,m |= (x. 3) 'in' (x. 0) )

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) = ( the Function of VAR,E +* ((x. 0),u)) . (x. 0) ) by A3, FUNCT_7:32;
( 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:32;
for x being Variable st (g +* ((x. 2),a)) . x <> g . x holds
x. 2 = x by FUNCT_7:32;
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:128;

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

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 :: thesis: ( ( E,h |= (x. 2) 'in' (x. 1) implies E,h |= All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))) ) & ( E,h |= All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))) implies E,h |= (x. 2) 'in' (x. 1) ) )

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 :: thesis: for m being Function of VAR,E st ( for x being Variable st m . x <> h . x holds
x. 3 = x ) holds
E,m |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))

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 :: thesis: ( E,m |= (x. 3) 'in' (x. 2) implies E,m |= (x. 3) 'in' (x. 0) )

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:32;
( (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 object ; :: 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:128;
for x being Variable st (h +* ((x. 3),a9)) . x <> h . x holds
x. 3 = x by FUNCT_7:32;
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:32;
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:32;
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:32;
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:23; :: thesis: verum