Theorem omex 9647

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

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 7889 and Fin = V (the universe of all sets) by fineqv 9261. 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 7900 through peano5 7905 (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 3454	. . 3 ⊢ 𝑥 ∈ V
2	1	ssex 5281	. 2 ⊢ (ω ⊆ 𝑥 → ω ∈ V)
3		zfinf2 9646	. . 3 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)
4		ax-1 6	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) → (𝑦 ∈ ω → (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)))
5	4	ralimi2 3094	. . . 4 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))
6		peano5 7905	. . . 4 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) → ω ⊆ 𝑥)
7	5, 6	sylan2 605	. . 3 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ω ⊆ 𝑥)
8	3, 7	eximii 1869	. 2 ⊢ ∃𝑥ω ⊆ 𝑥
9	2, 8	exlimiiv 1963	1 ⊢ ω ∈ V

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144  ∀wral 3076  Vcvv 3450   ⊆ wss 3895  ∅c0 4278  suc csuc 6364  ωcom 7877

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7751  ax-inf2 9645

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-tr 5212  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-om 7878

This theorem is used by:  axinf  9648  inf5  9649  omelon  9650  dfom3  9651  elom3  9652  oancom  9655  isfinite  9656  nnsdom  9658  omenps  9659  omensuc  9660  unbnn3  9663  noinfep  9664  ttrclse  9731  tz9.1  9733  tz9.1c  9734  dfhf2  9909  xpct  10098  fseqdom  10108  fseqen  10109  aleph0  10148  alephprc  10181  alephfplem1  10186  alephfplem4  10189  iunfictbso  10196  unctb  10285  cfom  10345  itunifval  10497  hsmexlem5  10511  axcc2lem  10517  acncc  10521  axcc4dom  10522  domtriomlem  10523  axdclem2  10601  fnct  10623  fnctOLD  10624  infinf  10654  unirnfdomd  10655  alephval2  10660  dominfac  10661  iunctb  10662  pwfseqlem4  10750  pwfseqlem5  10751  pwxpndom2  10753  pwdjundom  10755  gchac  10769  wunex2  10826  tskinf  10857  niex  10969  nnexALT  12340  ltweuz  14107  uzenom  14110  nnenom  14126  axdc4uzlem  14129  seqex  14149  rexpen  16401  cctop  23329  2ndcctbss  23779  2ndcdisj  23780  2ndcdisj2  23781  tx2ndc  23975  met2ndci  24846  n0sex  28708  n0ssold  28745  snct  33352  bnj852  35597  bnj865  35599  acwer1prc  35816  satf  36204  satom  36207  satfv0  36209  satfvsuclem1  36210  satfv1lem  36213  satf00  36225  satf0suclem  36226  satf0suc  36227  sat1el2xp  36230  fmla  36232  fmlasuc0  36235  ex-sategoelel  36272  ex-sategoelelomsuc  36277  ex-sategoelel12  36278  prv1n  36282  mirimanoffr  36546  bj-iomnnom  38273  iunctb2  38419  ctbssinf  38422  succlg  44423  finonex  44548  orbitex  46038