Theorem omex 9620

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

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 7850 and Fin = V (the universe of all sets) by fineqv 9246. 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 7861 through peano5 7866 (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 9619	. 2 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)
2		ax-1 6	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) → (𝑦 ∈ ω → (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)))
3	2	ralimi2 3077	. . . 4 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))
4		peano5 7866	. . . 4 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) → ω ⊆ 𝑥)
5	3, 4	sylan2 593	. . 3 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ω ⊆ 𝑥)
6	5	eximi 1837	. 2 ⊢ (∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ∃𝑥ω ⊆ 𝑥)
7		vex 3477	. . . 4 ⊢ 𝑥 ∈ V
8	7	ssex 5314	. . 3 ⊢ (ω ⊆ 𝑥 → ω ∈ V)
9	8	exlimiv 1933	. 2 ⊢ (∃𝑥ω ⊆ 𝑥 → ω ∈ V)
10	1, 6, 9	mp2b 10	1 ⊢ ω ∈ V

Syntax hints:   → wi 4   ∧ wa 396  ∃wex 1781   ∈ wcel 2106  ∀wral 3060  Vcvv 3473   ⊆ wss 3944  ∅c0 4318  suc csuc 6355  ωcom 7838

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5292  ax-nul 5299  ax-pr 5420  ax-un 7708  ax-inf2 9618

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  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 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4523  df-pw 4598  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-br 5142  df-opab 5204  df-tr 5259  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-ord 6356  df-on 6357  df-lim 6358  df-suc 6359  df-om 7839

This theorem is referenced by:  axinf  9621  inf5  9622  omelon  9623  dfom3  9624  elom3  9625  oancom  9628  isfinite  9629  nnsdom  9631  omenps  9632  omensuc  9633  unbnn3  9636  noinfep  9637  ttrclse  9704  tz9.1  9706  tz9.1c  9707  xpct  9993  fseqdom  10003  fseqen  10004  aleph0  10043  alephprc  10076  alephfplem1  10081  alephfplem4  10084  iunfictbso  10091  unctb  10182  r1om  10221  cfom  10241  itunifval  10393  hsmexlem5  10407  axcc2lem  10413  acncc  10417  axcc4dom  10418  domtriomlem  10419  axdclem2  10497  fnct  10514  infinf  10543  unirnfdomd  10544  alephval2  10549  dominfac  10550  iunctb  10551  pwfseqlem4  10639  pwfseqlem5  10640  pwxpndom2  10642  pwdjundom  10644  gchac  10658  wunex2  10715  tskinf  10746  niex  10858  nnexALT  12196  ltweuz  13908  uzenom  13911  nnenom  13927  axdc4uzlem  13930  seqex  13950  rexpen  16153  cctop  22438  2ndcctbss  22888  2ndcdisj  22889  2ndcdisj2  22890  tx2ndc  23084  met2ndci  23960  snct  31809  bnj852  33763  bnj865  33765  satf  34175  satom  34178  satfv0  34180  satfvsuclem1  34181  satfv1lem  34184  satf00  34196  satf0suclem  34197  satf0suc  34198  sat1el2xp  34201  fmla  34203  fmlasuc0  34206  ex-sategoelel  34243  ex-sategoelelomsuc  34248  ex-sategoelel12  34249  prv1n  34253  bj-iomnnom  35944  iunctb2  36088  ctbssinf  36091  succlg  41849  finonex  41976