Theorem omex 9100

Description: The existence of omega (the class of natural numbers). Axiom 7 of [TakeutiZaring] p. 43. This theorem is proved assuming the Axiom of Infinity and in fact is equivalent to it, as shown by the reverse derivation inf0 9078.

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 7585 and Fin = V (the universe of all sets) by fineqv 8727. 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 7595 through peano5 7599 (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 9099	. 2 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)
2		ax-1 6	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) → (𝑦 ∈ ω → (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)))
3	2	ralimi2 3157	. . . 4 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))
4		peano5 7599	. . . 4 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) → ω ⊆ 𝑥)
5	3, 4	sylan2 594	. . 3 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ω ⊆ 𝑥)
6	5	eximi 1831	. 2 ⊢ (∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ∃𝑥ω ⊆ 𝑥)
7		vex 3497	. . . 4 ⊢ 𝑥 ∈ V
8	7	ssex 5217	. . 3 ⊢ (ω ⊆ 𝑥 → ω ∈ V)
9	8	exlimiv 1927	. 2 ⊢ (∃𝑥ω ⊆ 𝑥 → ω ∈ V)
10	1, 6, 9	mp2b 10	1 ⊢ ω ∈ V

Syntax hints:   → wi 4   ∧ wa 398  ∃wex 1776   ∈ wcel 2110  ∀wral 3138  Vcvv 3494   ⊆ wss 3935  ∅c0 4290  suc csuc 6187  ωcom 7574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321  ax-un 7455  ax-inf2 9098

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-tp 4565  df-op 4567  df-uni 4832  df-br 5059  df-opab 5121  df-tr 5165  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-om 7575

This theorem is referenced by:  axinf  9101  inf5  9102  omelon  9103  dfom3  9104  elom3  9105  oancom  9108  isfinite  9109  nnsdom  9111  omenps  9112  omensuc  9113  unbnn3  9116  noinfep  9117  tz9.1  9165  tz9.1c  9166  xpct  9436  fseqdom  9446  fseqen  9447  aleph0  9486  alephprc  9519  alephfplem1  9524  alephfplem4  9527  iunfictbso  9534  unctb  9621  r1om  9660  cfom  9680  itunifval  9832  hsmexlem5  9846  axcc2lem  9852  acncc  9856  axcc4dom  9857  domtriomlem  9858  axdclem2  9936  fnct  9953  infinf  9982  unirnfdomd  9983  alephval2  9988  dominfac  9989  iunctb  9990  pwfseqlem4  10078  pwfseqlem5  10079  pwxpndom2  10081  pwdjundom  10083  gchac  10097  wunex2  10154  tskinf  10185  niex  10297  nnexALT  11634  ltweuz  13323  uzenom  13326  nnenom  13342  axdc4uzlem  13345  seqex  13365  rexpen  15575  cctop  21608  2ndcctbss  22057  2ndcdisj  22058  2ndcdisj2  22059  tx2ndc  22253  met2ndci  23126  snct  30443  bnj852  32188  bnj865  32190  satf  32595  satom  32598  satfv0  32600  satfvsuclem1  32601  satfv1lem  32604  satf00  32616  satf0suclem  32617  satf0suc  32618  sat1el2xp  32621  fmla  32623  fmlasuc0  32626  ex-sategoelel  32663  ex-sategoelelomsuc  32668  ex-sategoelel12  32669  prv1n  32673  trpredex  33071  bj-iomnnom  34535  iunctb2  34678  ctbssinf  34681