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. This
theorem is proved assuming the Axiom of
Infinity and in fact is equivalent to it, as shown by the reverse
derivation inf0 9150.
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 7604 and Fin = V (the universe of all sets) by fineqv 8805. 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 7614 through peano5 7618 (which many textbooks prove more easily assuming Infinity). (Contributed by NM, 6-Aug-1994.) |
Ref | Expression |
---|---|
omex | ⊢ ω ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zfinf2 9171 | . 2 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) | |
2 | ax-1 6 | . . . . 5 ⊢ ((𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) → (𝑦 ∈ ω → (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))) | |
3 | 2 | ralimi2 3072 | . . . 4 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) |
4 | peano5 7618 | . . . 4 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) → ω ⊆ 𝑥) | |
5 | 3, 4 | sylan2 596 | . . 3 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ω ⊆ 𝑥) |
6 | 5 | eximi 1841 | . 2 ⊢ (∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ∃𝑥ω ⊆ 𝑥) |
7 | vex 3401 | . . . 4 ⊢ 𝑥 ∈ V | |
8 | 7 | ssex 5186 | . . 3 ⊢ (ω ⊆ 𝑥 → ω ∈ V) |
9 | 8 | exlimiv 1936 | . 2 ⊢ (∃𝑥ω ⊆ 𝑥 → ω ∈ V) |
10 | 1, 6, 9 | mp2b 10 | 1 ⊢ ω ∈ V |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∃wex 1786 ∈ wcel 2113 ∀wral 3053 Vcvv 3397 ⊆ wss 3841 ∅c0 4209 suc csuc 6168 ωcom 7593 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2161 ax-12 2178 ax-ext 2710 ax-sep 5164 ax-nul 5171 ax-pr 5293 ax-un 7473 ax-inf2 9170 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2074 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-ral 3058 df-rex 3059 df-rab 3062 df-v 3399 df-dif 3844 df-un 3846 df-in 3848 df-ss 3858 df-pss 3860 df-nul 4210 df-if 4412 df-pw 4487 df-sn 4514 df-pr 4516 df-tp 4518 df-op 4520 df-uni 4794 df-br 5028 df-opab 5090 df-tr 5134 df-eprel 5430 df-po 5438 df-so 5439 df-fr 5478 df-we 5480 df-ord 6169 df-on 6170 df-lim 6171 df-suc 6172 df-om 7594 |
This theorem is referenced by: axinf 9173 inf5 9174 omelon 9175 dfom3 9176 elom3 9177 oancom 9180 isfinite 9181 nnsdom 9183 omenps 9184 omensuc 9185 unbnn3 9188 noinfep 9189 tz9.1 9237 tz9.1c 9238 xpct 9509 fseqdom 9519 fseqen 9520 aleph0 9559 alephprc 9592 alephfplem1 9597 alephfplem4 9600 iunfictbso 9607 unctb 9698 r1om 9737 cfom 9757 itunifval 9909 hsmexlem5 9923 axcc2lem 9929 acncc 9933 axcc4dom 9934 domtriomlem 9935 axdclem2 10013 fnct 10030 infinf 10059 unirnfdomd 10060 alephval2 10065 dominfac 10066 iunctb 10067 pwfseqlem4 10155 pwfseqlem5 10156 pwxpndom2 10158 pwdjundom 10160 gchac 10174 wunex2 10231 tskinf 10262 niex 10374 nnexALT 11711 ltweuz 13413 uzenom 13416 nnenom 13432 axdc4uzlem 13435 seqex 13455 rexpen 15666 cctop 21750 2ndcctbss 22199 2ndcdisj 22200 2ndcdisj2 22201 tx2ndc 22395 met2ndci 23268 snct 30615 bnj852 32464 bnj865 32466 satf 32878 satom 32881 satfv0 32883 satfvsuclem1 32884 satfv1lem 32887 satf00 32899 satf0suclem 32900 satf0suc 32901 sat1el2xp 32904 fmla 32906 fmlasuc0 32909 ex-sategoelel 32946 ex-sategoelelomsuc 32951 ex-sategoelel12 32952 prv1n 32956 trpredex 33371 bj-iomnnom 35040 iunctb2 35186 ctbssinf 35189 |
Copyright terms: Public domain | W3C validator |