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 A2:
( ( for
x being
Variable holds
( not
g . x <> f . x or
x. 0 = x or
x. 1
= x ) ) &
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;
A4:
(
(g +* (x. 2),v) . (x. 2) = v & ( for
x being
Variable st
x <> x. 2 holds
(g +* (x. 2),v) . x = g . x ) )
by FUNCT_7:34, FUNCT_7:130;
A5:
for
x being
Variable st
(g +* (x. 2),v) . x <> g . x holds
x. 2
= x
by A4;
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, ZF_MODEL:15;
then A6:
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 A5, ZF_MODEL:16;
(g +* (x. 2),v) . (x. 0 ) = g . (x. 0 )
by A4;
then
E,
g +* (x. 2),
v |= (x. 2) 'in' (x. 0 )
by A3, A4, 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 A6, ZF_MODEL:18;
then consider f being
Function of
VAR ,
E such that A7:
( ( for
x being
Variable st
f . x <> (g +* (x. 2),v) . x holds
x. 3
= x ) &
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;
take w =
f . (x. 3);
:: thesis: ( v c< w & w in u )
A8:
(
E,
f |= ((x. 3) 'in' (x. 0 )) '&' ('not' ((x. 3) '=' (x. 2))) &
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 A9:
a in v
;
:: thesis: a in w
v c= E
by A1;
then reconsider a' =
a as
Element of
E by A9;
set m =
f +* (x. 4),
a';
A10:
(
(f +* (x. 4),a') . (x. 4) = a' & ( for
x being
Variable st
x <> x. 4 holds
(f +* (x. 4),a') . x = f . x ) )
by FUNCT_7:34, FUNCT_7:130;
for
x being
Variable st
(f +* (x. 4),a') . x <> f . x holds
x. 4
= x
by A10;
then A11:
E,
f +* (x. 4),
a' |= ((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))
by A8, ZF_MODEL:16;
(
(f +* (x. 4),a') . (x. 2) = f . (x. 2) &
f . (x. 2) = (g +* (x. 2),v) . (x. 2) )
by A7, A10;
then
E,
f +* (x. 4),
a' |= (x. 4) 'in' (x. 2)
by A4, A9, A10, ZF_MODEL:13;
then
E,
f +* (x. 4),
a' |= (x. 4) 'in' (x. 3)
by A11, ZF_MODEL:18;
then
(f +* (x. 4),a') . (x. 4) in (f +* (x. 4),a') . (x. 3)
by ZF_MODEL:13;
hence
a in w
by A10;
:: thesis: verum
end;
A12:
(
E,
f |= (x. 3) 'in' (x. 0 ) &
E,
f |= 'not' ((x. 3) '=' (x. 2)) )
by A8, ZF_MODEL:15;
then
not
E,
f |= (x. 3) '=' (x. 2)
by ZF_MODEL:14;
then
(
f . (x. 3) <> f . (x. 2) &
f . (x. 2) = (g +* (x. 2),v) . (x. 2) )
by A7, ZF_MODEL:12;
hence
v <> w
by A4;
:: thesis: w in u
(
f . (x. 0 ) = (g +* (x. 2),v) . (x. 0 ) &
(g +* (x. 2),v) . (x. 0 ) = g . (x. 0 ) )
by A4, A7;
hence
w in u
by A12, ZF_MODEL:13;
:: thesis: verum
end;
given u being Element of E such that A13:
u <> {}
and
A14:
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 A13, 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;
A15:
( (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;
A16:
for x being Variable st (f0 +* (x. 0 ),u) . x <> f0 . x holds
x. 0 = x
by A15;
set f2 = (f0 +* (x. 0 ),u) +* (x. 1),a;
A17:
( ((f0 +* (x. 0 ),u) +* (x. 1),a) . (x. 1) = a & ( for x being Variable st x <> x. 1 holds
((f0 +* (x. 0 ),u) +* (x. 1),a) . x = (f0 +* (x. 0 ),u) . x ) )
by FUNCT_7:34, FUNCT_7:130;
A18:
for x being Variable st ((f0 +* (x. 0 ),u) +* (x. 1),a) . x <> (f0 +* (x. 0 ),u) . x holds
x. 1 = x
by A17;
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 A19:
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
(
f . (x. 2) in f . (x. 0 ) &
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 A17, A19, ZF_MODEL:13;
then consider w being
Element of
E such that A20:
(
f . (x. 2) c< w &
w in u )
by A14, A15;
A21:
(
f . (x. 2) c= w &
f . (x. 2) <> w )
by A20, XBOOLE_0:def 8;
set g =
f +* (x. 3),
w;
A22:
(
(f +* (x. 3),w) . (x. 3) = w & ( for
x being
Variable st
x <> x. 3 holds
(f +* (x. 3),w) . x = f . x ) )
by FUNCT_7:34, FUNCT_7:130;
A23:
for
x being
Variable st
(f +* (x. 3),w) . x <> f . x holds
x. 3
= x
by A22;
(
(f +* (x. 3),w) . (x. 0 ) = f . (x. 0 ) &
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 ) &
(f +* (x. 3),w) . (x. 2) = f . (x. 2) )
by A17, A19, A22;
then A24:
(
E,
f +* (x. 3),
w |= (x. 3) 'in' (x. 0 ) & not
E,
f +* (x. 3),
w |= (x. 3) '=' (x. 2) )
by A15, A20, A22, ZF_MODEL:12, ZF_MODEL:13;
then
E,
f +* (x. 3),
w |= 'not' ((x. 3) '=' (x. 2))
by ZF_MODEL:14;
then A25:
E,
f +* (x. 3),
w |= ((x. 3) 'in' (x. 0 )) '&' ('not' ((x. 3) '=' (x. 2)))
by A24, ZF_MODEL:15;
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 A26:
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
(
h . (x. 4) in h . (x. 2) &
h . (x. 2) = (f +* (x. 3),w) . (x. 2) &
(f +* (x. 3),w) . (x. 2) = f . (x. 2) )
by A22, A26, ZF_MODEL:13;
then
(
h . (x. 3) = (f +* (x. 3),w) . (x. 3) &
h . (x. 4) in w )
by A21, A26;
hence
E,
h |= (x. 4) 'in' (x. 3)
by A22, 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
E,
f +* (x. 3),
w |= All (x. 4),
(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))
by ZF_MODEL:16;
then
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 A25, 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 A23, 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 A27:
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. 0 ) = (f0 +* (x. 0 ),u) . (x. 0 )
by A17;
then
E,(f0 +* (x. 0 ),u) +* (x. 1),a |= (x. 1) 'in' (x. 0 )
by A13, A15, A17, ZF_MODEL:13;
then
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 A27, ZF_MODEL:15;
then
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 A18, ZF_MODEL:20;
hence
E,f0 |= the_axiom_of_infinity
by A16, ZF_MODEL:20; :: thesis: verum