let E be non empty set ; :: thesis: ( E is epsilon-transitive implies ( E |= the_axiom_of_unions iff for u being Element of E holds union 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_unions iff for u being Element of E holds union u in E )
thus ( E |= the_axiom_of_unions implies for u being Element of E holds union u in E ) :: thesis: ( ( for u being Element of E holds union u in E ) implies E |= the_axiom_of_unions )

proof

assume E |= the_axiom_of_unions ; :: thesis: for u being Element of E holds union u in E
then A2: E |= Ex (x. 1),(All (x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex (x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0 )))))) by ZF_MODEL:25;
let u be Element of E; :: thesis: union u in E
consider f0 being Function of VAR ,E;
set f = f0 +* (x. 0 ),u;
A3: ( (f0 +* (x. 0 ),u) . (x. 0 ) = u & ( for x being Variable st x <> x. 0 holds
(f0 +* (x. 0 ),u) . x = f0 . x ) ) by FUNCT_7:34, FUNCT_7:130;
E,f0 +* (x. 0 ),u |= Ex (x. 1),(All (x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex (x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0 )))))) by A2, ZF_MODEL:def 5;
then consider g being Function of VAR ,E such that
A4: ( ( for x being Variable st g . x <> (f0 +* (x. 0 ),u) . x holds
x. 1 = x ) & E,g |= All (x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex (x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0 ))))) ) by ZF_MODEL:20;
for a being set holds
( a in g . (x. 1) iff ex X being set st
( a in X & X in u ) )

proof

let a be set ; :: thesis: ( a in g . (x. 1) iff ex X being set st
( a in X & X in u ) )
thus ( a in g . (x. 1) implies ex X being set st
( a in X & X in u ) ) :: thesis: ( ex X being set st
( a in X & X in u ) implies a in g . (x. 1) )

proof

assume A5: a in g . (x. 1) ; :: thesis: ex X being set st
( a in X & X in u )
g . (x. 1) c= E by A1;
then reconsider a' = a as Element of E by A5;
set h = g +* (x. 2),a';
A6: ( (g +* (x. 2),a') . (x. 2) = a' & ( for x being Variable st x <> x. 2 holds
(g +* (x. 2),a') . x = g . x ) ) by FUNCT_7:34, FUNCT_7:130;
(g +* (x. 2),a') . (x. 1) = g . (x. 1) by A6;
then A7: E,g +* (x. 2),a' |= (x. 2) 'in' (x. 1) by A5, A6, ZF_MODEL:13;
for x being Variable st (g +* (x. 2),a') . x <> g . x holds
x. 2 = x by A6;
then E,g +* (x. 2),a' |= ((x. 2) 'in' (x. 1)) <=> (Ex (x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0 )))) by A4, ZF_MODEL:16;
then E,g +* (x. 2),a' |= Ex (x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0 ))) by A7, ZF_MODEL:19;
then consider m being Function of VAR ,E such that
A8: ( ( for x being Variable st m . x <> (g +* (x. 2),a') . x holds
x. 3 = x ) & E,m |= ((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0 )) ) by ZF_MODEL:20;
A9: ( E,m |= (x. 2) 'in' (x. 3) & E,m |= (x. 3) 'in' (x. 0 ) ) by A8, ZF_MODEL:15;
reconsider X = m . (x. 3) as set ;
take X ; :: thesis: ( a in X & X in u )
( m . (x. 0 ) = (g +* (x. 2),a') . (x. 0 ) & (g +* (x. 2),a') . (x. 0 ) = g . (x. 0 ) & g . (x. 0 ) = (f0 +* (x. 0 ),u) . (x. 0 ) & m . (x. 2) = (g +* (x. 2),a') . (x. 2) ) by A4, A6, A8;
hence ( a in X & X in u ) by A3, A6, A9, ZF_MODEL:13; :: thesis: verum

end;

given X being set such that A10: ( a in X & X in u ) ; :: thesis: a in g . (x. 1)
u c= E by A1;
then reconsider X = X as Element of E by A10;
X c= E by A1;
then reconsider a' = a as Element of E by A10;
set h = g +* (x. 2),a';
A11: ( (g +* (x. 2),a') . (x. 2) = a' & ( for x being Variable st x <> x. 2 holds
(g +* (x. 2),a') . x = g . x ) ) by FUNCT_7:34, FUNCT_7:130;
set m = (g +* (x. 2),a') +* (x. 3),X;
A12: ( ((g +* (x. 2),a') +* (x. 3),X) . (x. 3) = X & ( for x being Variable st x <> x. 3 holds
((g +* (x. 2),a') +* (x. 3),X) . x = (g +* (x. 2),a') . x ) ) by FUNCT_7:34, FUNCT_7:130;
A13: for x being Variable st ((g +* (x. 2),a') +* (x. 3),X) . x <> (g +* (x. 2),a') . x holds
x. 3 = x by A12;
( ((g +* (x. 2),a') +* (x. 3),X) . (x. 2) = (g +* (x. 2),a') . (x. 2) & ((g +* (x. 2),a') +* (x. 3),X) . (x. 0 ) = (g +* (x. 2),a') . (x. 0 ) & (g +* (x. 2),a') . (x. 0 ) = g . (x. 0 ) & g . (x. 0 ) = (f0 +* (x. 0 ),u) . (x. 0 ) ) by A4, A11, A12;
then ( E,(g +* (x. 2),a') +* (x. 3),X |= (x. 2) 'in' (x. 3) & E,(g +* (x. 2),a') +* (x. 3),X |= (x. 3) 'in' (x. 0 ) ) by A3, A10, A11, A12, ZF_MODEL:13;
then E,(g +* (x. 2),a') +* (x. 3),X |= ((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0 )) by ZF_MODEL:15;
then A14: E,g +* (x. 2),a' |= Ex (x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0 ))) by A13, ZF_MODEL:20;
for x being Variable st (g +* (x. 2),a') . x <> g . x holds
x. 2 = x by A11;
then E,g +* (x. 2),a' |= ((x. 2) 'in' (x. 1)) <=> (Ex (x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0 )))) by A4, ZF_MODEL:16;
then E,g +* (x. 2),a' |= (x. 2) 'in' (x. 1) by A14, ZF_MODEL:19;
then (g +* (x. 2),a') . (x. 2) in (g +* (x. 2),a') . (x. 1) by ZF_MODEL:13;
hence a in g . (x. 1) by A11; :: thesis: verum

end;

then g . (x. 1) = union u by TARSKI:def 4;
hence union u in E ; :: thesis: verum

end;

assume A15: for u being Element of E holds union u in E ; :: thesis: E |= the_axiom_of_unions

now

let f be Function of VAR ,E; :: thesis: E,f |= Ex (x. 1),(All (x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex (x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0 ))))))
reconsider v = union (f . (x. 0 )) as Element of E by A15;
set g = f +* (x. 1),v;
A16: ( (f +* (x. 1),v) . (x. 1) = v & ( for x being Variable st x <> x. 1 holds
(f +* (x. 1),v) . x = f . x ) ) by FUNCT_7:34, FUNCT_7:130;
A17: for x being Variable st (f +* (x. 1),v) . x <> f . x holds
x. 1 = x by A16;

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)) <=> (Ex (x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0 )))) )
assume A18: for x being Variable st h . x <> (f +* (x. 1),v) . x holds
x. 2 = x ; :: thesis: E,h |= ((x. 2) 'in' (x. 1)) <=> (Ex (x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0 ))))
then A19: h . (x. 1) = (f +* (x. 1),v) . (x. 1) ;
( E,h |= (x. 2) 'in' (x. 1) iff E,h |= Ex (x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0 ))) )

proof

thus ( E,h |= (x. 2) 'in' (x. 1) implies E,h |= Ex (x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0 ))) ) :: thesis: ( E,h |= Ex (x. 3),(((x. 2) 'in' (x. 3)) '&' ((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 |= Ex (x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0 )))
then h . (x. 2) in h . (x. 1) by ZF_MODEL:13;
then consider X being set such that
A20: ( h . (x. 2) in X & X in f . (x. 0 ) ) by A16, A19, TARSKI:def 4;
f . (x. 0 ) c= E by A1;
then reconsider X = X as Element of E by A20;
set m = h +* (x. 3),X;
A21: ( (h +* (x. 3),X) . (x. 3) = X & ( for x being Variable st x <> x. 3 holds
(h +* (x. 3),X) . x = h . x ) ) by FUNCT_7:34, FUNCT_7:130;
A22: for x being Variable st (h +* (x. 3),X) . x <> h . x holds
x. 3 = x by A21;
( (h +* (x. 3),X) . (x. 0 ) = h . (x. 0 ) & h . (x. 0 ) = (f +* (x. 1),v) . (x. 0 ) & (f +* (x. 1),v) . (x. 0 ) = f . (x. 0 ) & (h +* (x. 3),X) . (x. 2) = h . (x. 2) ) by A16, A18, A21;
then ( E,h +* (x. 3),X |= (x. 2) 'in' (x. 3) & E,h +* (x. 3),X |= (x. 3) 'in' (x. 0 ) ) by A20, A21, ZF_MODEL:13;
then E,h +* (x. 3),X |= ((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0 )) by ZF_MODEL:15;
hence E,h |= Ex (x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0 ))) by A22, ZF_MODEL:20; :: thesis: verum

end;

assume E,h |= Ex (x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0 ))) ; :: thesis: E,h |= (x. 2) 'in' (x. 1)
then consider m being Function of VAR ,E such that
A23: ( ( for x being Variable st m . x <> h . x holds
x. 3 = x ) & E,m |= ((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0 )) ) by ZF_MODEL:20;
( E,m |= (x. 2) 'in' (x. 3) & E,m |= (x. 3) 'in' (x. 0 ) ) by A23, ZF_MODEL:15;
then ( m . (x. 2) in m . (x. 3) & m . (x. 3) in m . (x. 0 ) ) by ZF_MODEL:13;
then A24: m . (x. 2) in union (m . (x. 0 )) by TARSKI:def 4;
( m . (x. 2) = h . (x. 2) & m . (x. 0 ) = h . (x. 0 ) & h . (x. 0 ) = (f +* (x. 1),v) . (x. 0 ) & (f +* (x. 1),v) . (x. 0 ) = f . (x. 0 ) & h . (x. 1) = (f +* (x. 1),v) . (x. 1) ) by A16, A18, A23;
hence E,h |= (x. 2) 'in' (x. 1) by A16, A24, ZF_MODEL:13; :: thesis: verum

end;

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

end;

then E,f +* (x. 1),v |= All (x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex (x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0 ))))) by ZF_MODEL:16;
hence E,f |= Ex (x. 1),(All (x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex (x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0 )))))) by A17, ZF_MODEL:20; :: thesis: verum

end;

then E |= Ex (x. 1),(All (x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex (x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0 )))))) by ZF_MODEL:def 5;
hence E |= the_axiom_of_unions by ZF_MODEL:25; :: thesis: verum