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

set f = the 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, the Function of VAR,E |= the_axiom_of_infinity ;
then consider g being Function of VAR,E such that
for x being Variable holds
( not g . x <> the Function of VAR,E . 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:22;
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:32, 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:128;
(g +* ((x. 2),v)) . (x. 0) = g . (x. 0) by FUNCT_7:32;
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 object ; :: 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:128;
for x being Variable st (f +* ((x. 4),a9)) . x <> f . x holds
x. 4 = x by FUNCT_7:32;
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:32;
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:32; :: 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:32;
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
set a = the Element of u;
u c= E by A1;
then reconsider a = the Element of u as Element of E by A15;
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:128;

now :: thesis: for f being Function of VAR,E st ( for x being Variable st f . x <> ((f0 +* ((x. 0),u)) +* ((x. 1),a)) . x holds
x. 2 = x ) holds
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))))))))

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

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:32;
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:128;
A23: f . (x. 2) c= w by A20;

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

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

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:32;
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:32;
(f +* ((x. 3),w)) . (x. 2) = f . (x. 2) by FUNCT_7:32;
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:32;
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:32, 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:32, FUNCT_7:128;
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:32, 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:32, ZF_MODEL:20;
hence E,f0 |= the_axiom_of_infinity by ZF_MODEL:20; :: thesis: verum