let W be Universe; :: thesis: ( omega in W implies W |= the_axiom_of_infinity )
assume omega in W ; :: thesis: W |= the_axiom_of_infinity
then reconsider u = omega as Element of W ;
now :: thesis: ex u being Element of W st
( u <> {} & ( for v being Element of W st v in u holds
ex w being Element of W st
( v c< w & w in u ) ) )
take u = u; :: thesis: ( u <> {} & ( for v being Element of W st v in u holds
ex w being Element of W st
( v c< w & w in u ) ) )
thus u <> {} ; :: thesis: for v being Element of W st v in u holds
ex w being Element of W st
( v c< w & w in u )
let v be Element of W; :: thesis: ( v in u implies ex w being Element of W st
( v c< w & w in u ) )
assume A1: v in u ; :: thesis: ex w being Element of W st
( v c< w & w in u )
then reconsider A = v as Ordinal ;
succ A in omega by A1, ORDINAL1:28;
then succ A c= u by ORDINAL1:def 2;
then reconsider w = succ A as Element of W by CLASSES1:def 1;
take w = w; :: thesis: ( v c< w & w in u )
A in succ A by ORDINAL1:6;
then ( v c= w & v <> w ) by ORDINAL1:def 2;
hence ( v c< w & w in u ) by A1, ORDINAL1:28; :: thesis: verum
end;
hence W |= the_axiom_of_infinity by ZFMODEL1:6; :: thesis: verum