![]() |
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 9658.
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 7898 and Fin = V (the universe of all sets) by fineqv 9296. 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 7910 through peano5 7915 (which many textbooks prove more easily assuming Infinity). (Contributed by NM, 6-Aug-1994.) |
Ref | Expression |
---|---|
omex | ⊢ ω ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zfinf2 9679 | . 2 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) | |
2 | ax-1 6 | . . . . 5 ⊢ ((𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) → (𝑦 ∈ ω → (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))) | |
3 | 2 | ralimi2 3075 | . . . 4 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) |
4 | peano5 7915 | . . . 4 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) → ω ⊆ 𝑥) | |
5 | 3, 4 | sylan2 593 | . . 3 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ω ⊆ 𝑥) |
6 | 5 | eximi 1831 | . 2 ⊢ (∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ∃𝑥ω ⊆ 𝑥) |
7 | vex 3481 | . . . 4 ⊢ 𝑥 ∈ V | |
8 | 7 | ssex 5326 | . . 3 ⊢ (ω ⊆ 𝑥 → ω ∈ V) |
9 | 8 | exlimiv 1927 | . 2 ⊢ (∃𝑥ω ⊆ 𝑥 → ω ∈ V) |
10 | 1, 6, 9 | mp2b 10 | 1 ⊢ ω ∈ V |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∃wex 1775 ∈ wcel 2105 ∀wral 3058 Vcvv 3477 ⊆ wss 3962 ∅c0 4338 suc csuc 6387 ωcom 7886 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-ext 2705 ax-sep 5301 ax-nul 5311 ax-pr 5437 ax-un 7753 ax-inf2 9678 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-ne 2938 df-ral 3059 df-rex 3068 df-rab 3433 df-v 3479 df-dif 3965 df-un 3967 df-in 3969 df-ss 3979 df-pss 3982 df-nul 4339 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4912 df-br 5148 df-opab 5210 df-tr 5265 df-eprel 5588 df-po 5596 df-so 5597 df-fr 5640 df-we 5642 df-ord 6388 df-on 6389 df-lim 6390 df-suc 6391 df-om 7887 |
This theorem is referenced by: axinf 9681 inf5 9682 omelon 9683 dfom3 9684 elom3 9685 oancom 9688 isfinite 9689 nnsdom 9691 omenps 9692 omensuc 9693 unbnn3 9696 noinfep 9697 ttrclse 9764 tz9.1 9766 tz9.1c 9767 xpct 10053 fseqdom 10063 fseqen 10064 aleph0 10103 alephprc 10136 alephfplem1 10141 alephfplem4 10144 iunfictbso 10151 unctb 10241 r1om 10280 cfom 10301 itunifval 10453 hsmexlem5 10467 axcc2lem 10473 acncc 10477 axcc4dom 10478 domtriomlem 10479 axdclem2 10557 fnct 10574 infinf 10603 unirnfdomd 10604 alephval2 10609 dominfac 10610 iunctb 10611 pwfseqlem4 10699 pwfseqlem5 10700 pwxpndom2 10702 pwdjundom 10704 gchac 10718 wunex2 10775 tskinf 10806 niex 10918 nnexALT 12265 ltweuz 13998 uzenom 14001 nnenom 14017 axdc4uzlem 14020 seqex 14040 rexpen 16260 cctop 23028 2ndcctbss 23478 2ndcdisj 23479 2ndcdisj2 23480 tx2ndc 23674 met2ndci 24550 snct 32730 bnj852 34913 bnj865 34915 satf 35337 satom 35340 satfv0 35342 satfvsuclem1 35343 satfv1lem 35346 satf00 35358 satf0suclem 35359 satf0suc 35360 sat1el2xp 35363 fmla 35365 fmlasuc0 35368 ex-sategoelel 35405 ex-sategoelelomsuc 35410 ex-sategoelel12 35411 prv1n 35415 bj-iomnnom 37241 iunctb2 37385 ctbssinf 37388 succlg 43317 finonex 43443 |
Copyright terms: Public domain | W3C validator |