| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > omex | Structured version Visualization version GIF version | ||
| 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 9578.
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 7862 and Fin = V (the universe of all sets) by fineqv 9215. 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 7873 through peano5 7878 (which many textbooks prove more easily assuming Infinity). (Contributed by NM, 6-Aug-1994.) |
| Ref | Expression |
|---|---|
| omex | ⊢ ω ∈ V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vex 3461 | . . 3 ⊢ 𝑥 ∈ V | |
| 2 | 1 | ssex 5282 | . 2 ⊢ (ω ⊆ 𝑥 → ω ∈ V) |
| 3 | zfinf2 9599 | . . 3 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) | |
| 4 | ax-1 6 | . . . . 5 ⊢ ((𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) → (𝑦 ∈ ω → (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))) | |
| 5 | 4 | ralimi2 3097 | . . . 4 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) |
| 6 | peano5 7878 | . . . 4 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) → ω ⊆ 𝑥) | |
| 7 | 5, 6 | sylan2 604 | . . 3 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ω ⊆ 𝑥) |
| 8 | 3, 7 | eximii 1860 | . 2 ⊢ ∃𝑥ω ⊆ 𝑥 |
| 9 | 2, 8 | exlimiiv 1954 | 1 ⊢ ω ∈ V |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 400 ∈ wcel 2145 ∀wral 3079 Vcvv 3457 ⊆ wss 3907 ∅c0 4288 suc csuc 6352 ωcom 7850 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-ext 2737 ax-sep 5251 ax-nul 5261 ax-pr 5395 ax-un 7722 ax-inf2 9598 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-sb 2094 df-clab 2744 df-cleq 2757 df-clel 2840 df-ne 2961 df-ral 3080 df-rex 3090 df-rab 3418 df-v 3459 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-pss 3927 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4869 df-br 5106 df-opab 5168 df-tr 5213 df-eprel 5552 df-po 5560 df-so 5561 df-fr 5605 df-we 5607 df-ord 6353 df-on 6354 df-lim 6355 df-suc 6356 df-om 7851 |
| This theorem is referenced by: axinf 9601 inf5 9602 omelon 9603 dfom3 9604 elom3 9605 oancom 9608 isfinite 9609 nnsdom 9611 omenps 9612 omensuc 9613 unbnn3 9616 noinfep 9617 ttrclse 9684 tz9.1 9686 tz9.1c 9687 xpct 9988 fseqdom 9998 fseqen 9999 aleph0 10038 alephprc 10071 alephfplem1 10076 alephfplem4 10079 iunfictbso 10086 unctb 10175 r1om 10214 cfom 10236 itunifval 10388 hsmexlem5 10402 axcc2lem 10408 acncc 10412 axcc4dom 10413 domtriomlem 10414 axdclem2 10492 fnct 10509 infinf 10539 unirnfdomd 10540 alephval2 10545 dominfac 10546 iunctb 10547 pwfseqlem4 10635 pwfseqlem5 10636 pwxpndom2 10638 pwdjundom 10640 gchac 10654 wunex2 10711 tskinf 10742 niex 10854 nnexALT 12226 ltweuz 13988 uzenom 13991 nnenom 14007 axdc4uzlem 14010 seqex 14030 rexpen 16274 cctop 23124 2ndcctbss 23573 2ndcdisj 23574 2ndcdisj2 23575 tx2ndc 23769 met2ndci 24640 n0sex 28468 n0ssold 28505 snct 32969 bnj852 35226 bnj865 35228 r1omfv 35418 satf 35716 satom 35719 satfv0 35721 satfvsuclem1 35722 satfv1lem 35725 satf00 35737 satf0suclem 35738 satf0suc 35739 sat1el2xp 35742 fmla 35744 fmlasuc0 35747 ex-sategoelel 35784 ex-sategoelelomsuc 35789 ex-sategoelel12 35790 prv1n 35794 bj-iomnnom 37763 iunctb2 37909 ctbssinf 37912 succlg 43917 finonex 44042 orbitex 45529 |
| Copyright terms: Public domain | W3C validator |