![]() |
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 9068.
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 7571 and Fin = V (the universe of all sets) by fineqv 8717. 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 7581 through peano5 7585 (which many textbooks prove more easily assuming Infinity). (Contributed by NM, 6-Aug-1994.) |
Ref | Expression |
---|---|
omex | ⊢ ω ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zfinf2 9089 | . 2 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) | |
2 | ax-1 6 | . . . . 5 ⊢ ((𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) → (𝑦 ∈ ω → (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))) | |
3 | 2 | ralimi2 3125 | . . . 4 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) |
4 | peano5 7585 | . . . 4 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) → ω ⊆ 𝑥) | |
5 | 3, 4 | sylan2 595 | . . 3 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ω ⊆ 𝑥) |
6 | 5 | eximi 1836 | . 2 ⊢ (∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ∃𝑥ω ⊆ 𝑥) |
7 | vex 3444 | . . . 4 ⊢ 𝑥 ∈ V | |
8 | 7 | ssex 5189 | . . 3 ⊢ (ω ⊆ 𝑥 → ω ∈ V) |
9 | 8 | exlimiv 1931 | . 2 ⊢ (∃𝑥ω ⊆ 𝑥 → ω ∈ V) |
10 | 1, 6, 9 | mp2b 10 | 1 ⊢ ω ∈ V |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∃wex 1781 ∈ wcel 2111 ∀wral 3106 Vcvv 3441 ⊆ wss 3881 ∅c0 4243 suc csuc 6161 ωcom 7560 |
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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pr 5295 ax-un 7441 ax-inf2 9088 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-ral 3111 df-rex 3112 df-rab 3115 df-v 3443 df-sbc 3721 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-pss 3900 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4801 df-br 5031 df-opab 5093 df-tr 5137 df-eprel 5430 df-po 5438 df-so 5439 df-fr 5478 df-we 5480 df-ord 6162 df-on 6163 df-lim 6164 df-suc 6165 df-om 7561 |
This theorem is referenced by: axinf 9091 inf5 9092 omelon 9093 dfom3 9094 elom3 9095 oancom 9098 isfinite 9099 nnsdom 9101 omenps 9102 omensuc 9103 unbnn3 9106 noinfep 9107 tz9.1 9155 tz9.1c 9156 xpct 9427 fseqdom 9437 fseqen 9438 aleph0 9477 alephprc 9510 alephfplem1 9515 alephfplem4 9518 iunfictbso 9525 unctb 9616 r1om 9655 cfom 9675 itunifval 9827 hsmexlem5 9841 axcc2lem 9847 acncc 9851 axcc4dom 9852 domtriomlem 9853 axdclem2 9931 fnct 9948 infinf 9977 unirnfdomd 9978 alephval2 9983 dominfac 9984 iunctb 9985 pwfseqlem4 10073 pwfseqlem5 10074 pwxpndom2 10076 pwdjundom 10078 gchac 10092 wunex2 10149 tskinf 10180 niex 10292 nnexALT 11627 ltweuz 13324 uzenom 13327 nnenom 13343 axdc4uzlem 13346 seqex 13366 rexpen 15573 cctop 21611 2ndcctbss 22060 2ndcdisj 22061 2ndcdisj2 22062 tx2ndc 22256 met2ndci 23129 snct 30475 bnj852 32303 bnj865 32305 satf 32713 satom 32716 satfv0 32718 satfvsuclem1 32719 satfv1lem 32722 satf00 32734 satf0suclem 32735 satf0suc 32736 sat1el2xp 32739 fmla 32741 fmlasuc0 32744 ex-sategoelel 32781 ex-sategoelelomsuc 32786 ex-sategoelel12 32787 prv1n 32791 trpredex 33189 bj-iomnnom 34674 iunctb2 34820 ctbssinf 34823 |
Copyright terms: Public domain | W3C validator |