Theorem omex 5542

Description: The existence of omega (the class of natural numbers). Axiom 7 of [TakeutiZaring] p. 43. This theorem is proved assuming the Axiom of Infinity and in fact is equivalent to it, as shown by the reverse derivation inf0 5521.

A finitist (someone who doesn't believe in infinity) could, without contradiction, replace the Axiom of Infinity by its denial -. om e. _V; this would lead to om = On (the proper class of ordinals) by omon 3774 and onprc 3676. The finitist could still develop natural number, integer, and rational number arithmetic but would be denied the real numbers (as well as much of the rest of mathematics). In deference to the finitist, much of our development is done, when possible, without invoking the Axiom of Infinity; an example is Peano's axioms peano1 3782 through peano5 3786 (which many textbooks prove more easily assuming Infinity).

Assertion

Ref	Expression
omex	|- om e. _V

Proof of Theorem omex

Step	Hyp	Ref	Expression
1		zfinf2 5541	. . 3 |- E.x((/) e. x /\ A.y e. x suc y e. x)
2		peano5 3786	. . . . 5 |- (((/) e. x /\ A.y e. om (y e. x -> suc y e. x)) -> om C_ x)
3		ax-1 4	. . . . . 6 |- ((y e. x -> suc y e. x) -> (y e. om -> (y e. x -> suc y e. x)))
4	3	ralimi2 1999	. . . . 5 |- (A.y e. x suc y e. x -> A.y e. om (y e. x -> suc y e. x))
5	2, 4	sylan2 498	. . . 4 |- (((/) e. x /\ A.y e. x suc y e. x) -> om C_ x)
6	5	eximi 1225	. . 3 |- (E.x((/) e. x /\ A.y e. x suc y e. x) -> E.xom C_ x)
7	1, 6	ax-mp 7	. 2 |- E.xom C_ x
8		visset 2128	. . . 4 |- x e. _V
9	8	ssex 3270	. . 3 |- (om C_ x -> om e. _V)
10	9	19.23aiv 1512	. 2 |- (E.xom C_ x -> om e. _V)
11	7, 10	ax-mp 7	1 |- om e. _V

Syntax hints:   -> wi 3   /\ wa 239   e. wcel 1138  E.wex 1164  A.wral 1939  _Vcvv 2125   C_ wss 2426  (/)c0 2701  suc csuc 3474  omcom 3760

This theorem is referenced by:  axinf 5543  inf5 5544  omelon 5545  dfom3 5546  elom3 5547  oancom 5549  isfinite 5550  nnsdom 5551  omenps 5552  omensuc 5553  unbnn3 5555  noinfep 5556  tz9.1 5562  aleph0 5670  sucdom 5790  alephprc 5837  alephfplem4 5843  alephval2 5846  dominf 5848  cfom 5860  cdainf 5883  niex 5957  nnenom 8562  xpomen 8564  unben 8569  aleph1re 8615  infxpidmlem10 8625  infdif 8632  iunctb 8639  aleph1irr 8642  bnj113 12250  trclex 13729  infxpg 14152  infsdomnng 14153  isfinite1b 14164  cptarc 14924  tarsuc2 14927  trclval 14953  fictb 15053  2ndcctbss 15160  neibastop2lem4 15204  ufilen 15261

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1142  ax-gen 1143  ax-8 1144  ax-9 1145  ax-10 1146  ax-11 1147  ax-12 1148  ax-13 1149  ax-14 1150  ax-17 1155  ax-4 1157  ax-5o 1159  ax-6o 1162  ax-9o 1319  ax-10o 1338  ax-16 1418  ax-11o 1426  ax-ext 1702  ax-sep 3253  ax-nul 3260  ax-pow 3296  ax-pr 3339  ax-un 3601  ax-inf2 5540

This theorem depends on definitions:  df-bi 163  df-or 240  df-an 241  df-3or 856  df-3an 857  df-ex 1165  df-sb 1374  df-eu 1613  df-mo 1614  df-clab 1709  df-cleq 1714  df-clel 1717  df-ne 1856  df-ral 1943  df-rex 1944  df-rab 1946  df-v 2127  df-dif 2430  df-un 2433  df-in 2436  df-ss 2438  df-pss 2440  df-nul 2702  df-if 2807  df-pw 2859  df-sn 2873  df-pr 2874  df-tp 2876  df-op 2877  df-uni 3000  df-br 3159  df-opab 3214  df-tr 3230  df-eprel 3398  df-po 3406  df-so 3419  df-fr 3440  df-we 3459  df-ord 3475  df-on 3476  df-lim 3477  df-suc 3478  df-om 3761

Copyright terms: Public domain