Theorem omex 9634

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

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 9259. 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 7874 through peano5 7879 (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		zfinf2 9633	. 2 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)
2		ax-1 6	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) → (𝑦 ∈ ω → (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)))
3	2	ralimi2 3079	. . . 4 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))
4		peano5 7879	. . . 4 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) → ω ⊆ 𝑥)
5	3, 4	sylan2 594	. . 3 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ω ⊆ 𝑥)
6	5	eximi 1838	. 2 ⊢ (∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ∃𝑥ω ⊆ 𝑥)
7		vex 3479	. . . 4 ⊢ 𝑥 ∈ V
8	7	ssex 5320	. . 3 ⊢ (ω ⊆ 𝑥 → ω ∈ V)
9	8	exlimiv 1934	. 2 ⊢ (∃𝑥ω ⊆ 𝑥 → ω ∈ V)
10	1, 6, 9	mp2b 10	1 ⊢ ω ∈ V

Syntax hints:   → wi 4   ∧ wa 397  ∃wex 1782   ∈ wcel 2107  ∀wral 3062  Vcvv 3475   ⊆ wss 3947  ∅c0 4321  suc csuc 6363  ωcom 7850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7720  ax-inf2 9632

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-tr 5265  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-om 7851

This theorem is referenced by:  axinf  9635  inf5  9636  omelon  9637  dfom3  9638  elom3  9639  oancom  9642  isfinite  9643  nnsdom  9645  omenps  9646  omensuc  9647  unbnn3  9650  noinfep  9651  ttrclse  9718  tz9.1  9720  tz9.1c  9721  xpct  10007  fseqdom  10017  fseqen  10018  aleph0  10057  alephprc  10090  alephfplem1  10095  alephfplem4  10098  iunfictbso  10105  unctb  10196  r1om  10235  cfom  10255  itunifval  10407  hsmexlem5  10421  axcc2lem  10427  acncc  10431  axcc4dom  10432  domtriomlem  10433  axdclem2  10511  fnct  10528  infinf  10557  unirnfdomd  10558  alephval2  10563  dominfac  10564  iunctb  10565  pwfseqlem4  10653  pwfseqlem5  10654  pwxpndom2  10656  pwdjundom  10658  gchac  10672  wunex2  10729  tskinf  10760  niex  10872  nnexALT  12210  ltweuz  13922  uzenom  13925  nnenom  13941  axdc4uzlem  13944  seqex  13964  rexpen  16167  cctop  22491  2ndcctbss  22941  2ndcdisj  22942  2ndcdisj2  22943  tx2ndc  23137  met2ndci  24013  snct  31916  bnj852  33870  bnj865  33872  satf  34282  satom  34285  satfv0  34287  satfvsuclem1  34288  satfv1lem  34291  satf00  34303  satf0suclem  34304  satf0suc  34305  sat1el2xp  34308  fmla  34310  fmlasuc0  34313  ex-sategoelel  34350  ex-sategoelelomsuc  34355  ex-sategoelel12  34356  prv1n  34360  bj-iomnnom  36078  iunctb2  36222  ctbssinf  36225  succlg  42011  finonex  42138