Theorem omex 8540

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

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 7076 and Fin = V (the universe of all sets) by fineqv 8175. 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 7085 through peano5 7089 (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 8539	. 2 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)
2		ax-1 6	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) → (𝑦 ∈ ω → (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)))
3	2	ralimi2 2949	. . . 4 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))
4		peano5 7089	. . . 4 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) → ω ⊆ 𝑥)
5	3, 4	sylan2 491	. . 3 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ω ⊆ 𝑥)
6	5	eximi 1762	. 2 ⊢ (∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ∃𝑥ω ⊆ 𝑥)
7		vex 3203	. . . 4 ⊢ 𝑥 ∈ V
8	7	ssex 4802	. . 3 ⊢ (ω ⊆ 𝑥 → ω ∈ V)
9	8	exlimiv 1858	. 2 ⊢ (∃𝑥ω ⊆ 𝑥 → ω ∈ V)
10	1, 6, 9	mp2b 10	1 ⊢ ω ∈ V

Syntax hints:   → wi 4   ∧ wa 384  ∃wex 1704   ∈ wcel 1990  ∀wral 2912  Vcvv 3200   ⊆ wss 3574  ∅c0 3915  suc csuc 5725  ωcom 7065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906  ax-un 6949  ax-inf2 8538

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-tr 4753  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-om 7066

This theorem is referenced by:  axinf  8541  inf5  8542  omelon  8543  dfom3  8544  elom3  8545  oancom  8548  isfinite  8549  nnsdom  8551  omenps  8552  omensuc  8553  unbnn3  8556  noinfep  8557  tz9.1  8605  tz9.1c  8606  xpct  8839  fseqdom  8849  fseqen  8850  aleph0  8889  alephprc  8922  alephfplem1  8927  alephfplem4  8930  iunfictbso  8937  unctb  9027  r1om  9066  cfom  9086  itunifval  9238  hsmexlem5  9252  axcc2lem  9258  acncc  9262  axcc4dom  9263  domtriomlem  9264  axdclem2  9342  fnct  9359  infinf  9388  unirnfdomd  9389  alephval2  9394  dominfac  9395  iunctb  9396  pwfseqlem4  9484  pwfseqlem5  9485  pwxpndom2  9487  pwcdandom  9489  gchac  9503  wunex2  9560  tskinf  9591  niex  9703  nnexALT  11022  ltweuz  12760  uzenom  12763  nnenom  12779  axdc4uzlem  12782  seqex  12803  rexpen  14957  cctop  20810  2ndcctbss  21258  2ndcdisj  21259  2ndcdisj2  21260  tx1stc  21453  tx2ndc  21454  met2ndci  22327  snct  29491  bnj852  30991  bnj865  30993  trpredex  31737