Theorem omex 8837

Description: The existence of omega (the class of natural numbers). Axiom 7 of [TakeutiZaring] p. 43. This theorem is proved assuming the Axiom of Infinity and in fact is equivalent to it, as shown by the reverse derivation inf0 8815.

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 7354 and Fin = V (the universe of all sets) by fineqv 8463. 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 7363 through peano5 7367 (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 8836	. 2 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)
2		ax-1 6	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) → (𝑦 ∈ ω → (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)))
3	2	ralimi2 3131	. . . 4 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))
4		peano5 7367	. . . 4 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) → ω ⊆ 𝑥)
5	3, 4	sylan2 586	. . 3 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ω ⊆ 𝑥)
6	5	eximi 1878	. 2 ⊢ (∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ∃𝑥ω ⊆ 𝑥)
7		vex 3401	. . . 4 ⊢ 𝑥 ∈ V
8	7	ssex 5039	. . 3 ⊢ (ω ⊆ 𝑥 → ω ∈ V)
9	8	exlimiv 1973	. 2 ⊢ (∃𝑥ω ⊆ 𝑥 → ω ∈ V)
10	1, 6, 9	mp2b 10	1 ⊢ ω ∈ V

Syntax hints:   → wi 4   ∧ wa 386  ∃wex 1823   ∈ wcel 2107  ∀wral 3090  Vcvv 3398   ⊆ wss 3792  ∅c0 4141  suc csuc 5978  ωcom 7343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pr 5138  ax-un 7226  ax-inf2 8835

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4672  df-br 4887  df-opab 4949  df-tr 4988  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-om 7344

This theorem is referenced by:  axinf  8838  inf5  8839  omelon  8840  dfom3  8841  elom3  8842  oancom  8845  isfinite  8846  nnsdom  8848  omenps  8849  omensuc  8850  unbnn3  8853  noinfep  8854  tz9.1  8902  tz9.1c  8903  xpct  9172  fseqdom  9182  fseqen  9183  aleph0  9222  alephprc  9255  alephfplem1  9260  alephfplem4  9263  iunfictbso  9270  unctb  9362  r1om  9401  cfom  9421  itunifval  9573  hsmexlem5  9587  axcc2lem  9593  acncc  9597  axcc4dom  9598  domtriomlem  9599  axdclem2  9677  fnct  9694  infinf  9723  unirnfdomd  9724  alephval2  9729  dominfac  9730  iunctb  9731  pwfseqlem4  9819  pwfseqlem5  9820  pwxpndom2  9822  pwcdandom  9824  gchac  9838  wunex2  9895  tskinf  9926  niex  10038  nnexALT  11376  ltweuz  13079  uzenom  13082  nnenom  13098  axdc4uzlem  13101  seqex  13121  rexpen  15361  cctop  21218  2ndcctbss  21667  2ndcdisj  21668  2ndcdisj2  21669  tx1stc  21862  tx2ndc  21863  met2ndci  22735  snct  30057  bnj852  31590  bnj865  31592  trpredex  32325  bj-iomnnom  33737