| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| 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 4615.
A finitist (someone who doesn't believe in infinity) could, without
contradiction, replace the Axiom of Infinity by its denial
|
| Ref | Expression |
|---|---|
| omex |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | zfinf 4635 |
. . 3
| |
| 2 | peano5 3159 |
. . . . 5
| |
| 3 | ax-1 4 |
. . . . . 6
| |
| 4 | 3 | r19.20i2 1706 |
. . . . 5
|
| 5 | 2, 4 | sylan2 453 |
. . . 4
|
| 6 | 5 | 19.22i 1042 |
. . 3
|
| 7 | 1, 6 | ax-mp 7 |
. 2
|
| 8 | visset 1816 |
. . . 4
| |
| 9 | 8 | ssex 2724 |
. . 3
|
| 10 | 9 | 19.23aiv 1297 |
. 2
|
| 11 | 7, 10 | ax-mp 7 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: inf5 4637 omelon 4638 dfom3 4639 elom3 4640 oancom 4642 isfinite 4643 isfiniteOLD 4644 nnsdom 4645 omenps 4646 omensuc 4647 unbnnt 4649 noinfep 4650 tz9.1 4656 sucdom 4852 sucdomOLD 4853 aleph0 4874 alephprc 4904 alephfplem4 4910 alephval2 4913 dominf 4915 dominfOLD 4916 cfom 4928 cdainf 4949 niex 5021 nnenom 7499 xpomen 7501 unben 7506 aleph1re 7552 infxpidmlem10 7562 infdif 7569 iunctb 7576 aleph1irr 7580 |
| 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 2708 ax-nul 2715 ax-pow 2748 ax-pr 2785 ax-un 2872 ax-inf2 4634 |
| 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 2052 df-un 2053 df-in 2054 df-ss 2056 df-nul 2284 df-if 2366 df-pw 2406 df-sn 2416 df-pr 2417 df-tp 2419 df-op 2420 df-uni 2508 df-br 2625 df-opab 2672 df-tr 2686 df-eprel 2838 df-po 2846 df-so 2856 df-fr 2923 df-we 2940 df-ord 2957 df-on 2958 df-lim 2959 df-suc 2960 df-om 3138 |