Theorem omex 4643

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

A finitist (someone who doesn't believe in infinity) could, without contradiction, replace the Axiom of Infinity by its denial -. om e. V; this would lead to om = On (the proper class of ordinals) by omon 3150 and onprc 2996. 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 3156 through peano5 3160 (which many textbooks prove more easily assuming Infinity).

Assertion

Ref	Expression
omex	|- om e. V

Proof of Theorem omex

Step	Hyp	Ref	Expression
1		zfinf 4642	. . 3 |- E.x((/) e. x /\ A.y e. x suc y e. x)
2		peano5 3160	. . . . 5 |- (((/) e. x /\ A.y e. om (y e. x -> suc y e. x)) -> om (_ x)
3		ax-1 4	. . . . . 6 |- ((y e. x -> suc y e. x) -> (y e. om -> (y e. x -> suc y e. x)))
4	3	r19.20i2 1706	. . . . 5 |- (A.y e. x suc y e. x -> A.y e. om (y e. x -> suc y e. x))
5	2, 4	sylan2 453	. . . 4 |- (((/) e. x /\ A.y e. x suc y e. x) -> om (_ x)
6	5	19.22i 1042	. . 3 |- (E.x((/) e. x /\ A.y e. x suc y e. x) -> E.xom (_ x)
7	1, 6	ax-mp 7	. 2 |- E.xom (_ x
8		visset 1816	. . . 4 |- x e. V
9	8	ssex 2725	. . 3 |- (om (_ x -> om e. V)
10	9	19.23aiv 1297	. 2 |- (E.xom (_ x -> om e. V)
11	7, 10	ax-mp 7	1 |- om e. V

Syntax hints:   -> wi 3   /\ wa 223   e. wcel 960  E.wex 982  A.wral 1648  Vcvv 1814   (_ wss 2051  (/)c0 2284  suc csuc 2957  omcom 3138

This theorem is referenced by:  inf5 4644  omelon 4645  dfom3 4646  elom3 4647  oancom 4649  isfinite 4650  isfiniteOLD 4651  nnsdom 4652  omenps 4653  omensuc 4654  unbnnt 4656  noinfep 4657  tz9.1 4663  sucdom 4859  sucdomOLD 4860  aleph0 4881  alephprc 4911  alephfplem4 4917  alephval2 4920  dominf 4922  dominfOLD 4923  cfom 4935  cdainf 4956  niex 5028  nnenom 7506  xpomen 7508  unben 7513  aleph1re 7559  infxpidmlem10 7569  infdif 7576  iunctb 7583  aleph1irr 7587

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-sep 2709  ax-nul 2716  ax-pow 2749  ax-pr 2786  ax-un 2873  ax-inf2 4641

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 778  df-3an 779  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-ral 1652  df-rex 1653  df-v 1815  df-dif 2053  df-un 2054  df-in 2055  df-ss 2057  df-nul 2285  df-if 2367  df-pw 2407  df-sn 2417  df-pr 2418  df-tp 2420  df-op 2421  df-uni 2509  df-br 2626  df-opab 2673  df-tr 2687  df-eprel 2839  df-po 2847  df-so 2857  df-fr 2924  df-we 2941  df-ord 2958  df-on 2959  df-lim 2960  df-suc 2961  df-om 3139

Copyright terms: Public domain