Theorem omex 6010

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 5988.

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 = _V (the universe of all sets) by fineqv 5874. 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 4137 through peano5 4141 (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 6009	. . 3 |- E.x((/) e. x /\ A.y e. x suc y e. x)
2		ax-1 4	. . . . . 6 |- ((y e. x -> suc y e. x) -> (y e. om -> (y e. x -> suc y e. x)))
3	2	ralimi2 2445	. . . . 5 |- (A.y e. x suc y e. x -> A.y e. om (y e. x -> suc y e. x))
4		peano5 4141	. . . . 5 |- (((/) e. x /\ A.y e. om (y e. x -> suc y e. x)) -> om C_ x)
5	3, 4	sylan2 696	. . . 4 |- (((/) e. x /\ A.y e. x suc y e. x) -> om C_ x)
6	5	eximi 1705	. . 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 2572	. . . 4 |- x e. _V
9	8	ssex 3654	. . 3 |- (om C_ x -> om e. _V)
10	9	19.23aiv 1972	. 2 |- (E.xom C_ x -> om e. _V)
11	7, 10	ax-mp 7	1 |- om e. _V

Syntax hints:   -> wi 3   /\ wa 433   e. wcel 1617  E.wex 1644  A.wral 2385  _Vcvv 2569   C_ wss 2859  (/)c0 3114  suc csuc 3845  omcom 4117

This theorem is referenced by:  axinf 6011  inf5 6012  isfinite3 6013  omelon 6014  omelonOLD 6015  dfom3 6016  elom3 6017  oancom 6020  isfinite 6021  nnsdom 6022  omenps 6023  omensuc 6024  unbnn3 6026  noinfep 6027  noinfepOLD 6028  tz9.1 6034  tz9.1c 6035  aleph0 6217  alephprc 6288  alephfplem4 6296  cdainf 6325  cfom 6344  axcc2lem 6360  axcc3 6362  axcc3OLD 6364  domtriomlem 6365  axdclem2 6446  sucdomOLD 6484  infxpidm 6491  alephval2 6521  dominfac 6522  cfomOLD 6525  cfpwsdom 6528  cdainfOLD 6531  niex 6604  nnenom 8208  xpnnen 9282  xpomenOLD 9284  qnnen 9287  aleph1re 9350  infdif 9367  iunctb 9374  aleph1irr 9377  unben 9523  bnj113 13398  trpredex 14836  infxpg 15395  infsdomnng 15396  isfinite1b 15407  cptarc 16313  tarsuc2 16316  trclval 16342  fictb 16456  2ndcctbss 16563  neibastop2lem4 16607  ufilen 16664

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-13 1628  ax-14 1629  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152  ax-sep 3638  ax-nul 3645  ax-pow 3681  ax-pr 3719  ax-un 3961  ax-inf2 6008

This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-3or 1131  df-3an 1132  df-ex 1645  df-sb 1845  df-eu 2070  df-mo 2071  df-clab 2158  df-cleq 2163  df-clel 2166  df-ne 2297  df-ral 2389  df-rex 2390  df-rab 2392  df-v 2571  df-dif 2862  df-un 2864  df-in 2866  df-ss 2868  df-pss 2870  df-nul 3115  df-if 3213  df-pw 3261  df-sn 3274  df-pr 3275  df-tp 3277  df-op 3278  df-uni 3399  df-br 3540  df-opab 3598  df-tr 3612  df-eprel 3776  df-po 3784  df-so 3796  df-fr 3814  df-we 3830  df-ord 3846  df-on 3847  df-lim 3848  df-suc 3849  df-om 4118

Copyright terms: Public domain