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 )

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;

( ((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

( 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

given u being Element of E such that A15:
u <> {}
and
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 )

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;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

A13:
E,f |= ((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))
by A7, ZF_MODEL:15;
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;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

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

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))))))))

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;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))))))))

end;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))))))) )

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: verumassume
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;

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;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))

then A27:
E,f +* ((x. 3),w) |= All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))
by ZF_MODEL:16;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))

end;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) )

hence
E,h |= ((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))
by ZF_MODEL:18; :: thesis: verumassume
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;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

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

( ((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