Theorem omex 9562

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

A finitist (someone who doesn't believe in infinity) could, without contradiction, replace the Axiom of Infinity by its denial ¬ ω ∈ V; this would lead to ω = On by omon 7825 and Fin = V (the universe of all sets) by fineqv 9174. 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 7836 through peano5 7840 (which many textbooks prove more easily assuming Infinity). (Contributed by NM, 6-Aug-1994.)

Assertion

Ref	Expression
omex	⊢ ω ∈ V

Proof of Theorem omex

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3436	. . 3 ⊢ 𝑥 ∈ V
2	1	ssex 5256	. 2 ⊢ (ω ⊆ 𝑥 → ω ∈ V)
3		zfinf2 9561	. . 3 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)
4		ax-1 6	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) → (𝑦 ∈ ω → (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)))
5	4	ralimi2 3072	. . . 4 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))
6		peano5 7840	. . . 4 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) → ω ⊆ 𝑥)
7	5, 6	sylan2 599	. . 3 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ω ⊆ 𝑥)
8	3, 7	eximii 1844	. 2 ⊢ ∃𝑥ω ⊆ 𝑥
9	2, 8	exlimiiv 1938	1 ⊢ ω ∈ V

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  ∀wral 3054  Vcvv 3432   ⊆ wss 3890  ∅c0 4268  suc csuc 6319  ωcom 7813

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369  ax-un 7685  ax-inf2 9560

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-tr 5187  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-om 7814

This theorem is referenced by:  axinf  9563  inf5  9564  omelon  9565  dfom3  9566  elom3  9567  oancom  9570  isfinite  9571  nnsdom  9573  omenps  9574  omensuc  9575  unbnn3  9578  noinfep  9579  ttrclse  9646  tz9.1  9648  tz9.1c  9649  xpct  9936  fseqdom  9946  fseqen  9947  aleph0  9986  alephprc  10019  alephfplem1  10024  alephfplem4  10027  iunfictbso  10034  unctb  10124  r1om  10163  cfom  10184  itunifval  10336  hsmexlem5  10350  axcc2lem  10356  acncc  10360  axcc4dom  10361  domtriomlem  10362  axdclem2  10440  fnct  10457  infinf  10487  unirnfdomd  10488  alephval2  10493  dominfac  10494  iunctb  10495  pwfseqlem4  10583  pwfseqlem5  10584  pwxpndom2  10586  pwdjundom  10588  gchac  10602  wunex2  10659  tskinf  10690  niex  10802  nnexALT  12174  ltweuz  13921  uzenom  13924  nnenom  13940  axdc4uzlem  13943  seqex  13963  rexpen  16193  cctop  22996  2ndcctbss  23445  2ndcdisj  23446  2ndcdisj2  23447  tx2ndc  23641  met2ndci  24512  n0sex  28334  n0ssold  28371  snct  32811  bnj852  35110  bnj865  35112  r1omfv  35298  satf  35588  satom  35591  satfv0  35593  satfvsuclem1  35594  satfv1lem  35597  satf00  35609  satf0suclem  35610  satf0suc  35611  sat1el2xp  35614  fmla  35616  fmlasuc0  35619  ex-sategoelel  35656  ex-sategoelelomsuc  35661  ex-sategoelel12  35662  prv1n  35666  bj-iomnnom  37626  iunctb2  37772  ctbssinf  37775  succlg  43780  finonex  43905  orbitex  45406