Theorem omex 9644

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

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 7871 and Fin = V (the universe of all sets) by fineqv 9269. 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 7883 through peano5 7888 (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 9643	. 2 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)
2		ax-1 6	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) → (𝑦 ∈ ω → (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)))
3	2	ralimi2 3077	. . . 4 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))
4		peano5 7888	. . . 4 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) → ω ⊆ 𝑥)
5	3, 4	sylan2 592	. . 3 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ω ⊆ 𝑥)
6	5	eximi 1836	. 2 ⊢ (∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ∃𝑥ω ⊆ 𝑥)
7		vex 3477	. . . 4 ⊢ 𝑥 ∈ V
8	7	ssex 5321	. . 3 ⊢ (ω ⊆ 𝑥 → ω ∈ V)
9	8	exlimiv 1932	. 2 ⊢ (∃𝑥ω ⊆ 𝑥 → ω ∈ V)
10	1, 6, 9	mp2b 10	1 ⊢ ω ∈ V

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1780   ∈ wcel 2105  ∀wral 3060  Vcvv 3473   ⊆ wss 3948  ∅c0 4322  suc csuc 6366  ωcom 7859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7729  ax-inf2 9642

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-tr 5266  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-om 7860

This theorem is referenced by:  axinf  9645  inf5  9646  omelon  9647  dfom3  9648  elom3  9649  oancom  9652  isfinite  9653  nnsdom  9655  omenps  9656  omensuc  9657  unbnn3  9660  noinfep  9661  ttrclse  9728  tz9.1  9730  tz9.1c  9731  xpct  10017  fseqdom  10027  fseqen  10028  aleph0  10067  alephprc  10100  alephfplem1  10105  alephfplem4  10108  iunfictbso  10115  unctb  10206  r1om  10245  cfom  10265  itunifval  10417  hsmexlem5  10431  axcc2lem  10437  acncc  10441  axcc4dom  10442  domtriomlem  10443  axdclem2  10521  fnct  10538  infinf  10567  unirnfdomd  10568  alephval2  10573  dominfac  10574  iunctb  10575  pwfseqlem4  10663  pwfseqlem5  10664  pwxpndom2  10666  pwdjundom  10668  gchac  10682  wunex2  10739  tskinf  10770  niex  10882  nnexALT  12221  ltweuz  13933  uzenom  13936  nnenom  13952  axdc4uzlem  13955  seqex  13975  rexpen  16178  cctop  22742  2ndcctbss  23192  2ndcdisj  23193  2ndcdisj2  23194  tx2ndc  23388  met2ndci  24264  snct  32220  bnj852  34245  bnj865  34247  satf  34657  satom  34660  satfv0  34662  satfvsuclem1  34663  satfv1lem  34666  satf00  34678  satf0suclem  34679  satf0suc  34680  sat1el2xp  34683  fmla  34685  fmlasuc0  34688  ex-sategoelel  34725  ex-sategoelelomsuc  34730  ex-sategoelel12  34731  prv1n  34735  bj-iomnnom  36456  iunctb2  36600  ctbssinf  36603  succlg  42393  finonex  42520