Theorem omex 9674

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

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 7916 and Fin = V (the universe of all sets) by fineqv 9289. 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 7927 through peano5 7932 (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 3458	. . 3 ⊢ 𝑥 ∈ V
2	1	ssex 5287	. 2 ⊢ (ω ⊆ 𝑥 → ω ∈ V)
3		zfinf2 9673	. . 3 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)
4		ax-1 6	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) → (𝑦 ∈ ω → (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)))
5	4	ralimi2 3098	. . . 4 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))
6		peano5 7932	. . . 4 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) → ω ⊆ 𝑥)
7	5, 6	sylan2 605	. . 3 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ω ⊆ 𝑥)
8	3, 7	eximii 1870	. 2 ⊢ ∃𝑥ω ⊆ 𝑥
9	2, 8	exlimiiv 1966	1 ⊢ ω ∈ V

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147  ∀wral 3080  Vcvv 3454   ⊆ wss 3900  ∅c0 4281  suc csuc 6385  ωcom 7904

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pr 5396  ax-un 7778  ax-inf2 9672

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5172  df-tr 5217  df-eprel 5556  df-po 5564  df-so 5565  df-fr 5609  df-we 5611  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-om 7905

This theorem is used by:  axinf  9675  inf5  9676  omelon  9677  dfom3  9678  elom3  9679  oancom  9682  isfinite  9683  nnsdom  9685  omenps  9686  omensuc  9687  unbnn3  9690  noinfep  9691  ttrclse  9758  tz9.1  9760  tz9.1c  9761  dfhf2  9936  xpct  10125  fseqdom  10135  fseqen  10136  aleph0  10175  alephprc  10208  alephfplem1  10213  alephfplem4  10216  iunfictbso  10223  unctb  10312  cfom  10372  itunifval  10524  hsmexlem5  10538  axcc2lem  10544  acncc  10548  axcc4dom  10549  domtriomlem  10550  axdclem2  10628  fnct  10650  fnctOLD  10651  infinf  10681  unirnfdomd  10682  alephval2  10687  dominfac  10688  iunctb  10689  pwfseqlem4  10777  pwfseqlem5  10778  pwxpndom2  10780  pwdjundom  10782  gchac  10796  wunex2  10853  tskinf  10884  niex  10996  nnexALT  12367  ltweuz  14134  uzenom  14137  nnenom  14153  axdc4uzlem  14156  seqex  14176  rexpen  16428  cctop  23357  2ndcctbss  23807  2ndcdisj  23808  2ndcdisj2  23809  tx2ndc  24003  met2ndci  24874  n0sex  28736  n0ssold  28773  snct  33379  bnj852  35634  bnj865  35636  acwer1prc  35865  satf  36298  satom  36301  satfv0  36303  satfvsuclem1  36304  satfv1lem  36307  satf00  36319  satf0suclem  36320  satf0suc  36321  sat1el2xp  36324  fmla  36326  fmlasuc0  36329  ex-sategoelel  36366  ex-sategoelelomsuc  36371  ex-sategoelel12  36372  prv1n  36376  mirimanoffr  36640  bj-iomnnom  38385  iunctb2  38531  ctbssinf  38534  succlg  44533  finonex  44658  orbitex  46151