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

set f0 = the Function of VAR,E;
assume A2: E |= the_axiom_of_unions ; :: thesis: for u being Element of E holds union u in E
let u be Element of E; :: thesis: union 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)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((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)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((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)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((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;
for a being object holds
( a in g . (x. 1) iff ex X being set st
( a in X & X in u ) )

proof

let a be object ; :: thesis: ( a in g . (x. 1) iff ex X being set st
( a in X & X in u ) )
A6: g . (x. 0) = ( the Function of VAR,E +* ((x. 0),u)) . (x. 0) by A3;
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 A7: 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 a9 = a as Element of E by A7;
set h = g +* ((x. 2),a9);
A8: (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 A9: E,g +* ((x. 2),a9) |= ((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((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 A7, A8, ZF_MODEL:13;
then E,g +* ((x. 2),a9) |= Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))) by A9, ZF_MODEL:19;
then consider m being Function of VAR,E such that
A10: for x being Variable st m . x <> (g +* ((x. 2),a9)) . x holds
x. 3 = x and
A11: E,m |= ((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)) by ZF_MODEL:20;
A12: ( m . (x. 0) = (g +* ((x. 2),a9)) . (x. 0) & m . (x. 2) = (g +* ((x. 2),a9)) . (x. 2) ) by A10;
reconsider X = m . (x. 3) as set ;
take X ; :: thesis: ( a in X & X in u )
A13: ( (g +* ((x. 2),a9)) . (x. 0) = g . (x. 0) & g . (x. 0) = ( the Function of VAR,E +* ((x. 0),u)) . (x. 0) ) by A3, FUNCT_7:32;
( E,m |= (x. 2) 'in' (x. 3) & E,m |= (x. 3) 'in' (x. 0) ) by A11, ZF_MODEL:15;
hence ( a in X & X in u ) by A5, A8, A13, A12, ZF_MODEL:13; :: thesis: verum

end;

given X being set such that A14: a in X and
A15: X in u ; :: thesis: a in g . (x. 1)
u c= E by A1;
then reconsider X = X as Element of E by A15;
X c= E by A1;
then reconsider a9 = a as Element of E by A14;
set h = g +* ((x. 2),a9);
set m = (g +* ((x. 2),a9)) +* ((x. 3),X);
A16: ((g +* ((x. 2),a9)) +* ((x. 3),X)) . (x. 3) = X by FUNCT_7:128;
( ((g +* ((x. 2),a9)) +* ((x. 3),X)) . (x. 0) = (g +* ((x. 2),a9)) . (x. 0) & (g +* ((x. 2),a9)) . (x. 0) = g . (x. 0) ) by FUNCT_7:32;
then A17: E,(g +* ((x. 2),a9)) +* ((x. 3),X) |= (x. 3) 'in' (x. 0) by A5, A15, A16, A6, ZF_MODEL:13;
A18: (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 A19: E,g +* ((x. 2),a9) |= ((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) by A4, ZF_MODEL:16;
((g +* ((x. 2),a9)) +* ((x. 3),X)) . (x. 2) = (g +* ((x. 2),a9)) . (x. 2) by FUNCT_7:32;
then E,(g +* ((x. 2),a9)) +* ((x. 3),X) |= (x. 2) 'in' (x. 3) by A14, A18, A16, ZF_MODEL:13;
then ( ( for x being Variable st ((g +* ((x. 2),a9)) +* ((x. 3),X)) . x <> (g +* ((x. 2),a9)) . x holds
x. 3 = x ) & E,(g +* ((x. 2),a9)) +* ((x. 3),X) |= ((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)) ) by A17, FUNCT_7:32, ZF_MODEL:15;
then E,g +* ((x. 2),a9) |= Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))) by ZF_MODEL:20;
then E,g +* ((x. 2),a9) |= (x. 2) 'in' (x. 1) by A19, ZF_MODEL:19;
then (g +* ((x. 2),a9)) . (x. 2) in (g +* ((x. 2),a9)) . (x. 1) by ZF_MODEL:13;
hence a in g . (x. 1) by A18, FUNCT_7:32; :: thesis: verum

end;

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

end;

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

now :: thesis: for f being Function of VAR,E holds 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)))))))))

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 A20;
set g = f +* ((x. 1),v);
A21: (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)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((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)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) )
assume A22: 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 A23: 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
A24: h . (x. 2) in X and
A25: X in f . (x. 0) by A21, A23, TARSKI:def 4;
f . (x. 0) c= E by A1;
then reconsider X = X as Element of E by A25;
set m = h +* ((x. 3),X);
A26: (h +* ((x. 3),X)) . (x. 3) = X by FUNCT_7:128;
A27: (f +* ((x. 1),v)) . (x. 0) = f . (x. 0) by FUNCT_7:32;
(h +* ((x. 3),X)) . (x. 2) = h . (x. 2) by FUNCT_7:32;
then A28: E,h +* ((x. 3),X) |= (x. 2) 'in' (x. 3) by A24, A26, ZF_MODEL:13;
( (h +* ((x. 3),X)) . (x. 0) = h . (x. 0) & h . (x. 0) = (f +* ((x. 1),v)) . (x. 0) ) by A22, FUNCT_7:32;
then E,h +* ((x. 3),X) |= (x. 3) 'in' (x. 0) by A25, A26, A27, ZF_MODEL:13;
then ( ( for x being Variable st (h +* ((x. 3),X)) . x <> h . x holds
x. 3 = x ) & E,h +* ((x. 3),X) |= ((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)) ) by A28, FUNCT_7:32, ZF_MODEL:15;
hence E,h |= Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))) by 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
A29: for x being Variable st m . x <> h . x holds
x. 3 = x and
A30: E,m |= ((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)) by ZF_MODEL:20;
E,m |= (x. 3) 'in' (x. 0) by A30, ZF_MODEL:15;
then A31: m . (x. 3) in m . (x. 0) by ZF_MODEL:13;
E,m |= (x. 2) 'in' (x. 3) by A30, ZF_MODEL:15;
then m . (x. 2) in m . (x. 3) by ZF_MODEL:13;
then A32: m . (x. 2) in union (m . (x. 0)) by A31, TARSKI:def 4;
A33: h . (x. 1) = (f +* ((x. 1),v)) . (x. 1) by A22;
A34: ( h . (x. 0) = (f +* ((x. 1),v)) . (x. 0) & (f +* ((x. 1),v)) . (x. 0) = f . (x. 0) ) by A22, FUNCT_7:32;
( m . (x. 2) = h . (x. 2) & m . (x. 0) = h . (x. 0) ) by A29;
hence E,h |= (x. 2) 'in' (x. 1) by A21, A32, A34, A33, 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 ( ( for x being Variable st (f +* ((x. 1),v)) . x <> f . x holds
x. 1 = x ) & 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 FUNCT_7:32, 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 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))))))))) ;
hence E |= the_axiom_of_unions by ZF_MODEL:23; :: thesis: verum