| 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 9657.
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 7895 and Fin = V (the universe of all sets) by fineqv 9295. 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 7906 through peano5 7911 (which many textbooks prove more easily assuming Infinity). (Contributed by NM, 6-Aug-1994.) |
| Ref | Expression |
|---|---|
| omex | ⊢ ω ∈ V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vex 3483 | . . 3 ⊢ 𝑥 ∈ V | |
| 2 | 1 | ssex 5319 | . 2 ⊢ (ω ⊆ 𝑥 → ω ∈ V) |
| 3 | zfinf2 9678 | . . 3 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) | |
| 4 | ax-1 6 | . . . . 5 ⊢ ((𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) → (𝑦 ∈ ω → (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))) | |
| 5 | 4 | ralimi2 3077 | . . . 4 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) |
| 6 | peano5 7911 | . . . 4 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) → ω ⊆ 𝑥) | |
| 7 | 5, 6 | sylan2 593 | . . 3 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ω ⊆ 𝑥) |
| 8 | 3, 7 | eximii 1837 | . 2 ⊢ ∃𝑥ω ⊆ 𝑥 |
| 9 | 2, 8 | exlimiiv 1931 | 1 ⊢ ω ∈ V |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2108 ∀wral 3060 Vcvv 3479 ⊆ wss 3950 ∅c0 4332 suc csuc 6384 ωcom 7883 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2707 ax-sep 5294 ax-nul 5304 ax-pr 5430 ax-un 7751 ax-inf2 9677 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2714 df-cleq 2728 df-clel 2815 df-ne 2940 df-ral 3061 df-rex 3070 df-rab 3436 df-v 3481 df-dif 3953 df-un 3955 df-in 3957 df-ss 3967 df-pss 3970 df-nul 4333 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4906 df-br 5142 df-opab 5204 df-tr 5258 df-eprel 5582 df-po 5590 df-so 5591 df-fr 5635 df-we 5637 df-ord 6385 df-on 6386 df-lim 6387 df-suc 6388 df-om 7884 |
| This theorem is referenced by: axinf 9680 inf5 9681 omelon 9682 dfom3 9683 elom3 9684 oancom 9687 isfinite 9688 nnsdom 9690 omenps 9691 omensuc 9692 unbnn3 9695 noinfep 9696 ttrclse 9763 tz9.1 9765 tz9.1c 9766 xpct 10052 fseqdom 10062 fseqen 10063 aleph0 10102 alephprc 10135 alephfplem1 10140 alephfplem4 10143 iunfictbso 10150 unctb 10240 r1om 10279 cfom 10300 itunifval 10452 hsmexlem5 10466 axcc2lem 10472 acncc 10476 axcc4dom 10477 domtriomlem 10478 axdclem2 10556 fnct 10573 infinf 10602 unirnfdomd 10603 alephval2 10608 dominfac 10609 iunctb 10610 pwfseqlem4 10698 pwfseqlem5 10699 pwxpndom2 10701 pwdjundom 10703 gchac 10717 wunex2 10774 tskinf 10805 niex 10917 nnexALT 12264 ltweuz 13998 uzenom 14001 nnenom 14017 axdc4uzlem 14020 seqex 14040 rexpen 16260 cctop 23003 2ndcctbss 23453 2ndcdisj 23454 2ndcdisj2 23455 tx2ndc 23649 met2ndci 24525 snct 32714 bnj852 34913 bnj865 34915 satf 35336 satom 35339 satfv0 35341 satfvsuclem1 35342 satfv1lem 35345 satf00 35357 satf0suclem 35358 satf0suc 35359 sat1el2xp 35362 fmla 35364 fmlasuc0 35367 ex-sategoelel 35404 ex-sategoelelomsuc 35409 ex-sategoelel12 35410 prv1n 35414 bj-iomnnom 37238 iunctb2 37382 ctbssinf 37385 succlg 43319 finonex 43445 |
| Copyright terms: Public domain | W3C validator |