Theorem omex 9600

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

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 7862 and Fin = V (the universe of all sets) by fineqv 9215. 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 7873 through peano5 7878 (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 3461	. . 3 ⊢ 𝑥 ∈ V
2	1	ssex 5281	. 2 ⊢ (ω ⊆ 𝑥 → ω ∈ V)
3		zfinf2 9599	. . 3 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)
4		ax-1 6	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) → (𝑦 ∈ ω → (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)))
5	4	ralimi2 3097	. . . 4 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))
6		peano5 7878	. . . 4 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) → ω ⊆ 𝑥)
7	5, 6	sylan2 604	. . 3 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ω ⊆ 𝑥)
8	3, 7	eximii 1860	. 2 ⊢ ∃𝑥ω ⊆ 𝑥
9	2, 8	exlimiiv 1954	1 ⊢ ω ∈ V

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2145  ∀wral 3079  Vcvv 3457   ⊆ wss 3907  ∅c0 4288  suc csuc 6351  ωcom 7850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5250  ax-nul 5260  ax-pr 5394  ax-un 7722  ax-inf2 9598

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-opab 5167  df-tr 5212  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6352  df-on 6353  df-lim 6354  df-suc 6355  df-om 7851

This theorem is referenced by:  axinf  9601  inf5  9602  omelon  9603  dfom3  9604  elom3  9605  oancom  9608  isfinite  9609  nnsdom  9611  omenps  9612  omensuc  9613  unbnn3  9616  noinfep  9617  ttrclse  9684  tz9.1  9686  tz9.1c  9687  xpct  9988  fseqdom  9998  fseqen  9999  aleph0  10038  alephprc  10071  alephfplem1  10076  alephfplem4  10079  iunfictbso  10086  unctb  10175  r1om  10214  cfom  10236  itunifval  10388  hsmexlem5  10402  axcc2lem  10408  acncc  10412  axcc4dom  10413  domtriomlem  10414  axdclem2  10492  fnct  10509  infinf  10539  unirnfdomd  10540  alephval2  10545  dominfac  10546  iunctb  10547  pwfseqlem4  10635  pwfseqlem5  10636  pwxpndom2  10638  pwdjundom  10640  gchac  10654  wunex2  10711  tskinf  10742  niex  10854  nnexALT  12223  ltweuz  13985  uzenom  13988  nnenom  14004  axdc4uzlem  14007  seqex  14027  rexpen  16272  cctop  23120  2ndcctbss  23569  2ndcdisj  23570  2ndcdisj2  23571  tx2ndc  23765  met2ndci  24636  n0sex  28464  n0ssold  28501  snct  32965  bnj852  35221  bnj865  35223  r1omfv  35413  satf  35711  satom  35714  satfv0  35716  satfvsuclem1  35717  satfv1lem  35720  satf00  35732  satf0suclem  35733  satf0suc  35734  sat1el2xp  35737  fmla  35739  fmlasuc0  35742  ex-sategoelel  35779  ex-sategoelelomsuc  35784  ex-sategoelel12  35785  prv1n  35789  bj-iomnnom  37758  iunctb2  37904  ctbssinf  37907  succlg  43912  finonex  44037  orbitex  45523