Theorem omex 9564

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

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 7830 and Fin = V (the universe of all sets) by fineqv 9179. 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 7841 through peano5 7845 (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 3446	. . 3 ⊢ 𝑥 ∈ V
2	1	ssex 5268	. 2 ⊢ (ω ⊆ 𝑥 → ω ∈ V)
3		zfinf2 9563	. . 3 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)
4		ax-1 6	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) → (𝑦 ∈ ω → (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)))
5	4	ralimi2 3070	. . . 4 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))
6		peano5 7845	. . . 4 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) → ω ⊆ 𝑥)
7	5, 6	sylan2 594	. . 3 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ω ⊆ 𝑥)
8	3, 7	eximii 1839	. 2 ⊢ ∃𝑥ω ⊆ 𝑥
9	2, 8	exlimiiv 1933	1 ⊢ ω ∈ V

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∀wral 3052  Vcvv 3442   ⊆ wss 3903  ∅c0 4287  suc csuc 6327  ωcom 7818

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379  ax-un 7690  ax-inf2 9562

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-tr 5208  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-om 7819

This theorem is referenced by:  axinf  9565  inf5  9566  omelon  9567  dfom3  9568  elom3  9569  oancom  9572  isfinite  9573  nnsdom  9575  omenps  9576  omensuc  9577  unbnn3  9580  noinfep  9581  ttrclse  9648  tz9.1  9650  tz9.1c  9651  xpct  9938  fseqdom  9948  fseqen  9949  aleph0  9988  alephprc  10021  alephfplem1  10026  alephfplem4  10029  iunfictbso  10036  unctb  10126  r1om  10165  cfom  10186  itunifval  10338  hsmexlem5  10352  axcc2lem  10358  acncc  10362  axcc4dom  10363  domtriomlem  10364  axdclem2  10442  fnct  10459  infinf  10489  unirnfdomd  10490  alephval2  10495  dominfac  10496  iunctb  10497  pwfseqlem4  10585  pwfseqlem5  10586  pwxpndom2  10588  pwdjundom  10590  gchac  10604  wunex2  10661  tskinf  10692  niex  10804  nnexALT  12159  ltweuz  13896  uzenom  13899  nnenom  13915  axdc4uzlem  13918  seqex  13938  rexpen  16165  cctop  22962  2ndcctbss  23411  2ndcdisj  23412  2ndcdisj2  23413  tx2ndc  23607  met2ndci  24478  n0sex  28325  n0ssold  28362  snct  32801  bnj852  35096  bnj865  35098  r1omfv  35285  satf  35566  satom  35569  satfv0  35571  satfvsuclem1  35572  satfv1lem  35575  satf00  35587  satf0suclem  35588  satf0suc  35589  sat1el2xp  35592  fmla  35594  fmlasuc0  35597  ex-sategoelel  35634  ex-sategoelelomsuc  35639  ex-sategoelel12  35640  prv1n  35644  bj-iomnnom  37511  iunctb2  37655  ctbssinf  37658  succlg  43682  finonex  43807  orbitex  45308