let E be non empty set ; :: thesis: ( E is epsilon-transitive implies ( E |= the_axiom_of_infinity iff ex u being Element of E st
( u <> {} & ( for v being Element of E st v in u holds
ex w being Element of E st
( v c< w & w in u ) ) ) ) )
assume A1: for X being set st X in E holds
X c= E ; :: according to ORDINAL1:def 2 :: thesis: ( E |= the_axiom_of_infinity iff ex u being Element of E st
( u <> {} & ( for v being Element of E st v in u holds
ex w being Element of E st
( v c< w & w in u ) ) ) )
thus ( E |= the_axiom_of_infinity implies ex u being Element of E st
( u <> {} & ( for v being Element of E st v in u holds
ex w being Element of E st
( v c< w & w in u ) ) ) ) :: thesis: ( ex u being Element of E st
( u <> {} & ( for v being Element of E st v in u holds
ex w being Element of E st
( v c< w & w in u ) ) ) implies E |= the_axiom_of_infinity )

proof

consider f being Function of VAR ,E;
assume for g being Function of VAR ,E holds E,g |= the_axiom_of_infinity ; :: according to ZF_MODEL:def 5 :: thesis: ex u being Element of E st
( u <> {} & ( for v being Element of E st v in u holds
ex w being Element of E st
( v c< w & w in u ) ) )
then E,f |= the_axiom_of_infinity ;
then consider g being Function of VAR ,E such that
for x being Variable holds
( not g . x <> f . x or x. 0 = x or x. 1 = x ) and
A2: E,g |= ((x. 1) 'in' (x. 0 )) '&' (All (x. 2),(((x. 2) 'in' (x. 0 )) => (Ex (x. 3),((((x. 3) 'in' (x. 0 )) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All (x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))) by ZF_MODEL:23;
take u = g . (x. 0 ); :: thesis: ( u <> {} & ( for v being Element of E st v in u holds
ex w being Element of E st
( v c< w & w in u ) ) )
E,g |= (x. 1) 'in' (x. 0 ) by A2, ZF_MODEL:15;
hence u <> {} by ZF_MODEL:13; :: thesis: for v being Element of E st v in u holds
ex w being Element of E st
( v c< w & w in u )
let v be Element of E; :: thesis: ( v in u implies ex w being Element of E st
( v c< w & w in u ) )
assume A3: v in u ; :: thesis: ex w being Element of E st
( v c< w & w in u )
set h = g +* (x. 2),v;
( ( for x being Variable st (g +* (x. 2),v) . x <> g . x holds
x. 2 = x ) & E,g |= All (x. 2),(((x. 2) 'in' (x. 0 )) => (Ex (x. 3),((((x. 3) 'in' (x. 0 )) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All (x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))) ) by A2, FUNCT_7:34, ZF_MODEL:15;
then A4: E,g +* (x. 2),v |= ((x. 2) 'in' (x. 0 )) => (Ex (x. 3),((((x. 3) 'in' (x. 0 )) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All (x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))) by ZF_MODEL:16;
A5: (g +* (x. 2),v) . (x. 2) = v by FUNCT_7:130;
(g +* (x. 2),v) . (x. 0 ) = g . (x. 0 ) by FUNCT_7:34;
then E,g +* (x. 2),v |= (x. 2) 'in' (x. 0 ) by A3, A5, ZF_MODEL:13;
then E,g +* (x. 2),v |= Ex (x. 3),((((x. 3) 'in' (x. 0 )) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All (x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))) by A4, ZF_MODEL:18;
then consider f being Function of VAR ,E such that
A6: for x being Variable st f . x <> (g +* (x. 2),v) . x holds
x. 3 = x and
A7: E,f |= (((x. 3) 'in' (x. 0 )) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All (x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))) by ZF_MODEL:20;
A8: f . (x. 0 ) = (g +* (x. 2),v) . (x. 0 ) by A6;
take w = f . (x. 3); :: thesis: ( v c< w & w in u )
A9: E,f |= All (x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))) by A7, ZF_MODEL:15;
thus v c= w :: according to XBOOLE_0:def 8 :: thesis: ( not v = w & w in u )

proof

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

end;

A13: E,f |= ((x. 3) 'in' (x. 0 )) '&' ('not' ((x. 3) '=' (x. 2))) by A7, ZF_MODEL:15;
then E,f |= 'not' ((x. 3) '=' (x. 2)) by ZF_MODEL:15;
then not E,f |= (x. 3) '=' (x. 2) by ZF_MODEL:14;
then f . (x. 3) <> f . (x. 2) by ZF_MODEL:12;
hence v <> w by A5, A6; :: thesis: w in u
A14: (g +* (x. 2),v) . (x. 0 ) = g . (x. 0 ) by FUNCT_7:34;
E,f |= (x. 3) 'in' (x. 0 ) by A13, ZF_MODEL:15;
hence w in u by A8, A14, ZF_MODEL:13; :: thesis: verum

end;

given u being Element of E such that A15: u <> {} and
A16: for v being Element of E st v in u holds
ex w being Element of E st
( v c< w & w in u ) ; :: thesis: E |= the_axiom_of_infinity
consider a being Element of u;
u c= E by A1;
then reconsider a = a as Element of E by A15, TARSKI:def 3;
let f0 be Function of VAR ,E; :: according to ZF_MODEL:def 5 :: thesis: E,f0 |= the_axiom_of_infinity
set f1 = f0 +* (x. 0 ),u;
set f2 = (f0 +* (x. 0 ),u) +* (x. 1),a;
A17: (f0 +* (x. 0 ),u) . (x. 0 ) = u by FUNCT_7:130;

now

let f be Function of VAR ,E; :: thesis: ( ( for x being Variable st f . x <> ((f0 +* (x. 0 ),u) +* (x. 1),a) . x holds
x. 2 = x ) implies E,f |= ((x. 2) 'in' (x. 0 )) => (Ex (x. 3),((((x. 3) 'in' (x. 0 )) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All (x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))) )
assume A18: for x being Variable st f . x <> ((f0 +* (x. 0 ),u) +* (x. 1),a) . x holds
x. 2 = x ; :: thesis: E,f |= ((x. 2) 'in' (x. 0 )) => (Ex (x. 3),((((x. 3) 'in' (x. 0 )) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All (x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))

now

assume E,f |= (x. 2) 'in' (x. 0 ) ; :: thesis: E,f |= Ex (x. 3),((((x. 3) 'in' (x. 0 )) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All (x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))
then A19: f . (x. 2) in f . (x. 0 ) by ZF_MODEL:13;
( f . (x. 0 ) = ((f0 +* (x. 0 ),u) +* (x. 1),a) . (x. 0 ) & ((f0 +* (x. 0 ),u) +* (x. 1),a) . (x. 0 ) = (f0 +* (x. 0 ),u) . (x. 0 ) ) by A18, FUNCT_7:34;
then consider w being Element of E such that
A20: f . (x. 2) c< w and
A21: w in u by A16, A17, A19;
set g = f +* (x. 3),w;
A22: (f +* (x. 3),w) . (x. 3) = w by FUNCT_7:130;
A23: f . (x. 2) c= w by A20, XBOOLE_0:def 8;

now

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

now

assume E,h |= (x. 4) 'in' (x. 2) ; :: thesis: E,h |= (x. 4) 'in' (x. 3)
then A25: h . (x. 4) in h . (x. 2) by ZF_MODEL:13;
A26: h . (x. 3) = (f +* (x. 3),w) . (x. 3) by A24;
( h . (x. 2) = (f +* (x. 3),w) . (x. 2) & (f +* (x. 3),w) . (x. 2) = f . (x. 2) ) by A24, FUNCT_7:34;
hence E,h |= (x. 4) 'in' (x. 3) by A23, A22, A25, A26, ZF_MODEL:13; :: thesis: verum

end;

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

end;

then A27: E,f +* (x. 3),w |= All (x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))) by ZF_MODEL:16;
A28: ((f0 +* (x. 0 ),u) +* (x. 1),a) . (x. 0 ) = (f0 +* (x. 0 ),u) . (x. 0 ) by FUNCT_7:34;
(f +* (x. 3),w) . (x. 2) = f . (x. 2) by FUNCT_7:34;
then not E,f +* (x. 3),w |= (x. 3) '=' (x. 2) by A20, A22, ZF_MODEL:12;
then A29: E,f +* (x. 3),w |= 'not' ((x. 3) '=' (x. 2)) by ZF_MODEL:14;
( (f +* (x. 3),w) . (x. 0 ) = f . (x. 0 ) & f . (x. 0 ) = ((f0 +* (x. 0 ),u) +* (x. 1),a) . (x. 0 ) ) by A18, FUNCT_7:34;
then E,f +* (x. 3),w |= (x. 3) 'in' (x. 0 ) by A17, A21, A22, A28, ZF_MODEL:13;
then E,f +* (x. 3),w |= ((x. 3) 'in' (x. 0 )) '&' ('not' ((x. 3) '=' (x. 2))) by A29, ZF_MODEL:15;
then ( ( for x being Variable st (f +* (x. 3),w) . x <> f . x holds
x. 3 = x ) & E,f +* (x. 3),w |= (((x. 3) 'in' (x. 0 )) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All (x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))) ) by A27, FUNCT_7:34, ZF_MODEL:15;
hence E,f |= Ex (x. 3),((((x. 3) 'in' (x. 0 )) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All (x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))) by ZF_MODEL:20; :: thesis: verum

end;

hence E,f |= ((x. 2) 'in' (x. 0 )) => (Ex (x. 3),((((x. 3) 'in' (x. 0 )) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All (x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))) by ZF_MODEL:18; :: thesis: verum

end;

then A30: E,(f0 +* (x. 0 ),u) +* (x. 1),a |= All (x. 2),(((x. 2) 'in' (x. 0 )) => (Ex (x. 3),((((x. 3) 'in' (x. 0 )) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All (x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))) by ZF_MODEL:16;
( ((f0 +* (x. 0 ),u) +* (x. 1),a) . (x. 1) = a & ((f0 +* (x. 0 ),u) +* (x. 1),a) . (x. 0 ) = (f0 +* (x. 0 ),u) . (x. 0 ) ) by FUNCT_7:34, FUNCT_7:130;
then E,(f0 +* (x. 0 ),u) +* (x. 1),a |= (x. 1) 'in' (x. 0 ) by A15, A17, ZF_MODEL:13;
then ( ( for x being Variable st ((f0 +* (x. 0 ),u) +* (x. 1),a) . x <> (f0 +* (x. 0 ),u) . x holds
x. 1 = x ) & E,(f0 +* (x. 0 ),u) +* (x. 1),a |= ((x. 1) 'in' (x. 0 )) '&' (All (x. 2),(((x. 2) 'in' (x. 0 )) => (Ex (x. 3),((((x. 3) 'in' (x. 0 )) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All (x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))) ) by A30, FUNCT_7:34, ZF_MODEL:15;
then ( ( for x being Variable st (f0 +* (x. 0 ),u) . x <> f0 . x holds
x. 0 = x ) & E,f0 +* (x. 0 ),u |= Ex (x. 1),(((x. 1) 'in' (x. 0 )) '&' (All (x. 2),(((x. 2) 'in' (x. 0 )) => (Ex (x. 3),((((x. 3) 'in' (x. 0 )) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All (x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))) ) by FUNCT_7:34, ZF_MODEL:20;
hence E,f0 |= the_axiom_of_infinity by ZF_MODEL:20; :: thesis: verum