![]() |
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 9598.
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 7850 and Fin = V (the universe of all sets) by fineqv 9246. 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 7861 through peano5 7866 (which many textbooks prove more easily assuming Infinity). (Contributed by NM, 6-Aug-1994.) |
Ref | Expression |
---|---|
omex | ⊢ ω ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zfinf2 9619 | . 2 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) | |
2 | ax-1 6 | . . . . 5 ⊢ ((𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) → (𝑦 ∈ ω → (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))) | |
3 | 2 | ralimi2 3077 | . . . 4 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) |
4 | peano5 7866 | . . . 4 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) → ω ⊆ 𝑥) | |
5 | 3, 4 | sylan2 593 | . . 3 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ω ⊆ 𝑥) |
6 | 5 | eximi 1837 | . 2 ⊢ (∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ∃𝑥ω ⊆ 𝑥) |
7 | vex 3477 | . . . 4 ⊢ 𝑥 ∈ V | |
8 | 7 | ssex 5314 | . . 3 ⊢ (ω ⊆ 𝑥 → ω ∈ V) |
9 | 8 | exlimiv 1933 | . 2 ⊢ (∃𝑥ω ⊆ 𝑥 → ω ∈ V) |
10 | 1, 6, 9 | mp2b 10 | 1 ⊢ ω ∈ V |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∃wex 1781 ∈ wcel 2106 ∀wral 3060 Vcvv 3473 ⊆ wss 3944 ∅c0 4318 suc csuc 6355 ωcom 7838 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2702 ax-sep 5292 ax-nul 5299 ax-pr 5420 ax-un 7708 ax-inf2 9618 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-ne 2940 df-ral 3061 df-rex 3070 df-rab 3432 df-v 3475 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3963 df-nul 4319 df-if 4523 df-pw 4598 df-sn 4623 df-pr 4625 df-op 4629 df-uni 4902 df-br 5142 df-opab 5204 df-tr 5259 df-eprel 5573 df-po 5581 df-so 5582 df-fr 5624 df-we 5626 df-ord 6356 df-on 6357 df-lim 6358 df-suc 6359 df-om 7839 |
This theorem is referenced by: axinf 9621 inf5 9622 omelon 9623 dfom3 9624 elom3 9625 oancom 9628 isfinite 9629 nnsdom 9631 omenps 9632 omensuc 9633 unbnn3 9636 noinfep 9637 ttrclse 9704 tz9.1 9706 tz9.1c 9707 xpct 9993 fseqdom 10003 fseqen 10004 aleph0 10043 alephprc 10076 alephfplem1 10081 alephfplem4 10084 iunfictbso 10091 unctb 10182 r1om 10221 cfom 10241 itunifval 10393 hsmexlem5 10407 axcc2lem 10413 acncc 10417 axcc4dom 10418 domtriomlem 10419 axdclem2 10497 fnct 10514 infinf 10543 unirnfdomd 10544 alephval2 10549 dominfac 10550 iunctb 10551 pwfseqlem4 10639 pwfseqlem5 10640 pwxpndom2 10642 pwdjundom 10644 gchac 10658 wunex2 10715 tskinf 10746 niex 10858 nnexALT 12196 ltweuz 13908 uzenom 13911 nnenom 13927 axdc4uzlem 13930 seqex 13950 rexpen 16153 cctop 22438 2ndcctbss 22888 2ndcdisj 22889 2ndcdisj2 22890 tx2ndc 23084 met2ndci 23960 snct 31809 bnj852 33763 bnj865 33765 satf 34175 satom 34178 satfv0 34180 satfvsuclem1 34181 satfv1lem 34184 satf00 34196 satf0suclem 34197 satf0suc 34198 sat1el2xp 34201 fmla 34203 fmlasuc0 34206 ex-sategoelel 34243 ex-sategoelelomsuc 34248 ex-sategoelel12 34249 prv1n 34253 bj-iomnnom 35944 iunctb2 36088 ctbssinf 36091 succlg 41849 finonex 41976 |
Copyright terms: Public domain | W3C validator |