Theorem omex 9679

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

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 7895 and Fin = V (the universe of all sets) by fineqv 9295. 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 7906 through peano5 7911 (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 3483	. . 3 ⊢ 𝑥 ∈ V
2	1	ssex 5319	. 2 ⊢ (ω ⊆ 𝑥 → ω ∈ V)
3		zfinf2 9678	. . 3 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)
4		ax-1 6	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) → (𝑦 ∈ ω → (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)))
5	4	ralimi2 3077	. . . 4 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))
6		peano5 7911	. . . 4 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) → ω ⊆ 𝑥)
7	5, 6	sylan2 593	. . 3 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ω ⊆ 𝑥)
8	3, 7	eximii 1837	. 2 ⊢ ∃𝑥ω ⊆ 𝑥
9	2, 8	exlimiiv 1931	1 ⊢ ω ∈ V

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∀wral 3060  Vcvv 3479   ⊆ wss 3950  ∅c0 4332  suc csuc 6384  ωcom 7883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5294  ax-nul 5304  ax-pr 5430  ax-un 7751  ax-inf2 9677

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2728  df-clel 2815  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4906  df-br 5142  df-opab 5204  df-tr 5258  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5635  df-we 5637  df-ord 6385  df-on 6386  df-lim 6387  df-suc 6388  df-om 7884

This theorem is referenced by:  axinf  9680  inf5  9681  omelon  9682  dfom3  9683  elom3  9684  oancom  9687  isfinite  9688  nnsdom  9690  omenps  9691  omensuc  9692  unbnn3  9695  noinfep  9696  ttrclse  9763  tz9.1  9765  tz9.1c  9766  xpct  10052  fseqdom  10062  fseqen  10063  aleph0  10102  alephprc  10135  alephfplem1  10140  alephfplem4  10143  iunfictbso  10150  unctb  10240  r1om  10279  cfom  10300  itunifval  10452  hsmexlem5  10466  axcc2lem  10472  acncc  10476  axcc4dom  10477  domtriomlem  10478  axdclem2  10556  fnct  10573  infinf  10602  unirnfdomd  10603  alephval2  10608  dominfac  10609  iunctb  10610  pwfseqlem4  10698  pwfseqlem5  10699  pwxpndom2  10701  pwdjundom  10703  gchac  10717  wunex2  10774  tskinf  10805  niex  10917  nnexALT  12264  ltweuz  13998  uzenom  14001  nnenom  14017  axdc4uzlem  14020  seqex  14040  rexpen  16260  cctop  23003  2ndcctbss  23453  2ndcdisj  23454  2ndcdisj2  23455  tx2ndc  23649  met2ndci  24525  snct  32714  bnj852  34913  bnj865  34915  satf  35336  satom  35339  satfv0  35341  satfvsuclem1  35342  satfv1lem  35345  satf00  35357  satf0suclem  35358  satf0suc  35359  sat1el2xp  35362  fmla  35364  fmlasuc0  35367  ex-sategoelel  35404  ex-sategoelelomsuc  35409  ex-sategoelel12  35410  prv1n  35414  bj-iomnnom  37238  iunctb2  37382  ctbssinf  37385  succlg  43319  finonex  43445