Theorem omex 9595

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

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 7854 and Fin = V (the universe of all sets) by fineqv 9207. 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 7865 through peano5 7870 (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 3457	. . 3 ⊢ 𝑥 ∈ V
2	1	ssex 5276	. 2 ⊢ (ω ⊆ 𝑥 → ω ∈ V)
3		zfinf2 9594	. . 3 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)
4		ax-1 6	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) → (𝑦 ∈ ω → (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)))
5	4	ralimi2 3093	. . . 4 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))
6		peano5 7870	. . . 4 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) → ω ⊆ 𝑥)
7	5, 6	sylan2 602	. . 3 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ω ⊆ 𝑥)
8	3, 7	eximii 1856	. 2 ⊢ ∃𝑥ω ⊆ 𝑥
9	2, 8	exlimiiv 1950	1 ⊢ ω ∈ V

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2141  ∀wral 3075  Vcvv 3453   ⊆ wss 3904  ∅c0 4285  suc csuc 6344  ωcom 7842

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pr 5389  ax-un 7714  ax-inf2 9593

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-tr 5207  df-eprel 5545  df-po 5553  df-so 5554  df-fr 5598  df-we 5600  df-ord 6345  df-on 6346  df-lim 6347  df-suc 6348  df-om 7843

This theorem is referenced by:  axinf  9596  inf5  9597  omelon  9598  dfom3  9599  elom3  9600  oancom  9603  isfinite  9604  nnsdom  9606  omenps  9607  omensuc  9608  unbnn3  9611  noinfep  9612  ttrclse  9679  tz9.1  9681  tz9.1c  9682  xpct  9969  fseqdom  9979  fseqen  9980  aleph0  10019  alephprc  10052  alephfplem1  10057  alephfplem4  10060  iunfictbso  10067  unctb  10157  r1om  10196  cfom  10218  itunifval  10370  hsmexlem5  10384  axcc2lem  10390  acncc  10394  axcc4dom  10395  domtriomlem  10396  axdclem2  10474  fnct  10491  infinf  10521  unirnfdomd  10522  alephval2  10527  dominfac  10528  iunctb  10529  pwfseqlem4  10617  pwfseqlem5  10618  pwxpndom2  10620  pwdjundom  10622  gchac  10636  wunex2  10693  tskinf  10724  niex  10836  nnexALT  12209  ltweuz  13971  uzenom  13974  nnenom  13990  axdc4uzlem  13993  seqex  14013  rexpen  16243  cctop  23046  2ndcctbss  23495  2ndcdisj  23496  2ndcdisj2  23497  tx2ndc  23691  met2ndci  24562  n0sex  28387  n0ssold  28424  snct  32864  bnj852  35180  bnj865  35182  r1omfv  35370  satf  35667  satom  35670  satfv0  35672  satfvsuclem1  35673  satfv1lem  35676  satf00  35688  satf0suclem  35689  satf0suc  35690  sat1el2xp  35693  fmla  35695  fmlasuc0  35698  ex-sategoelel  35735  ex-sategoelelomsuc  35740  ex-sategoelel12  35741  prv1n  35745  bj-iomnnom  37715  iunctb2  37861  ctbssinf  37864  succlg  43869  finonex  43994  orbitex  45495