Theorem omex 9558

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

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 7818 and Fin = V (the universe of all sets) by fineqv 9168. 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 7829 through peano5 7833 (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 3442	. . 3 ⊢ 𝑥 ∈ V
2	1	ssex 5263	. 2 ⊢ (ω ⊆ 𝑥 → ω ∈ V)
3		zfinf2 9557	. . 3 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)
4		ax-1 6	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) → (𝑦 ∈ ω → (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)))
5	4	ralimi2 3061	. . . 4 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))
6		peano5 7833	. . . 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 2109  ∀wral 3044  Vcvv 3438   ⊆ wss 3905  ∅c0 4286  suc csuc 6313  ωcom 7806

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7675  ax-inf2 9556

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-tr 5203  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-om 7807

This theorem is referenced by:  axinf  9559  inf5  9560  omelon  9561  dfom3  9562  elom3  9563  oancom  9566  isfinite  9567  nnsdom  9569  omenps  9570  omensuc  9571  unbnn3  9574  noinfep  9575  ttrclse  9642  tz9.1  9644  tz9.1c  9645  xpct  9929  fseqdom  9939  fseqen  9940  aleph0  9979  alephprc  10012  alephfplem1  10017  alephfplem4  10020  iunfictbso  10027  unctb  10117  r1om  10156  cfom  10177  itunifval  10329  hsmexlem5  10343  axcc2lem  10349  acncc  10353  axcc4dom  10354  domtriomlem  10355  axdclem2  10433  fnct  10450  infinf  10479  unirnfdomd  10480  alephval2  10485  dominfac  10486  iunctb  10487  pwfseqlem4  10575  pwfseqlem5  10576  pwxpndom2  10578  pwdjundom  10580  gchac  10594  wunex2  10651  tskinf  10682  niex  10794  nnexALT  12148  ltweuz  13886  uzenom  13889  nnenom  13905  axdc4uzlem  13908  seqex  13928  rexpen  16155  cctop  22909  2ndcctbss  23358  2ndcdisj  23359  2ndcdisj2  23360  tx2ndc  23554  met2ndci  24426  snct  32670  bnj852  34890  bnj865  34892  satf  35328  satom  35331  satfv0  35333  satfvsuclem1  35334  satfv1lem  35337  satf00  35349  satf0suclem  35350  satf0suc  35351  sat1el2xp  35354  fmla  35356  fmlasuc0  35359  ex-sategoelel  35396  ex-sategoelelomsuc  35401  ex-sategoelel12  35402  prv1n  35406  bj-iomnnom  37235  iunctb2  37379  ctbssinf  37382  succlg  43304  finonex  43430  orbitex  44932