Theorem omex 9655

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

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 7882 through peano5 7887 (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 3463	. . 3 ⊢ 𝑥 ∈ V
2	1	ssex 5291	. 2 ⊢ (ω ⊆ 𝑥 → ω ∈ V)
3		zfinf2 9654	. . 3 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)
4		ax-1 6	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) → (𝑦 ∈ ω → (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)))
5	4	ralimi2 3068	. . . 4 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))
6		peano5 7887	. . . 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 3051  Vcvv 3459   ⊆ wss 3926  ∅c0 4308  suc csuc 6354  ωcom 7859

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 5266  ax-nul 5276  ax-pr 5402  ax-un 7727  ax-inf2 9653

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-tr 5230  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-om 7860

This theorem is referenced by:  axinf  9656  inf5  9657  omelon  9658  dfom3  9659  elom3  9660  oancom  9663  isfinite  9664  nnsdom  9666  omenps  9667  omensuc  9668  unbnn3  9671  noinfep  9672  ttrclse  9739  tz9.1  9741  tz9.1c  9742  xpct  10028  fseqdom  10038  fseqen  10039  aleph0  10078  alephprc  10111  alephfplem1  10116  alephfplem4  10119  iunfictbso  10126  unctb  10216  r1om  10255  cfom  10276  itunifval  10428  hsmexlem5  10442  axcc2lem  10448  acncc  10452  axcc4dom  10453  domtriomlem  10454  axdclem2  10532  fnct  10549  infinf  10578  unirnfdomd  10579  alephval2  10584  dominfac  10585  iunctb  10586  pwfseqlem4  10674  pwfseqlem5  10675  pwxpndom2  10677  pwdjundom  10679  gchac  10693  wunex2  10750  tskinf  10781  niex  10893  nnexALT  12240  ltweuz  13977  uzenom  13980  nnenom  13996  axdc4uzlem  13999  seqex  14019  rexpen  16244  cctop  22942  2ndcctbss  23391  2ndcdisj  23392  2ndcdisj2  23393  tx2ndc  23587  met2ndci  24459  snct  32637  bnj852  34898  bnj865  34900  satf  35321  satom  35324  satfv0  35326  satfvsuclem1  35327  satfv1lem  35330  satf00  35342  satf0suclem  35343  satf0suc  35344  sat1el2xp  35347  fmla  35349  fmlasuc0  35352  ex-sategoelel  35389  ex-sategoelelomsuc  35394  ex-sategoelel12  35395  prv1n  35399  bj-iomnnom  37223  iunctb2  37367  ctbssinf  37370  succlg  43299  finonex  43425  orbitex  44928