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 9379.
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 7724 and Fin = V (the universe of all sets) by fineqv 9038. 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 7735 through peano5 7740 (which many textbooks prove more easily assuming Infinity). (Contributed by NM, 6-Aug-1994.) |
Ref | Expression |
---|---|
omex | ⊢ ω ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zfinf2 9400 | . 2 ⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) | |
2 | ax-1 6 | . . . . 5 ⊢ ((𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥) → (𝑦 ∈ ω → (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))) | |
3 | 2 | ralimi2 3084 | . . . 4 ⊢ (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) |
4 | peano5 7740 | . . . 4 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥)) → ω ⊆ 𝑥) | |
5 | 3, 4 | sylan2 593 | . . 3 ⊢ ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ω ⊆ 𝑥) |
6 | 5 | eximi 1837 | . 2 ⊢ (∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ∃𝑥ω ⊆ 𝑥) |
7 | vex 3436 | . . . 4 ⊢ 𝑥 ∈ V | |
8 | 7 | ssex 5245 | . . 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 1782 ∈ wcel 2106 ∀wral 3064 Vcvv 3432 ⊆ wss 3887 ∅c0 4256 suc csuc 6268 ωcom 7712 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-11 2154 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pr 5352 ax-un 7588 ax-inf2 9399 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-ne 2944 df-ral 3069 df-rex 3070 df-rab 3073 df-v 3434 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-br 5075 df-opab 5137 df-tr 5192 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-om 7713 |
This theorem is referenced by: axinf 9402 inf5 9403 omelon 9404 dfom3 9405 elom3 9406 oancom 9409 isfinite 9410 nnsdom 9412 omenps 9413 omensuc 9414 unbnn3 9417 noinfep 9418 ttrclse 9485 tz9.1 9487 tz9.1c 9488 xpct 9772 fseqdom 9782 fseqen 9783 aleph0 9822 alephprc 9855 alephfplem1 9860 alephfplem4 9863 iunfictbso 9870 unctb 9961 r1om 10000 cfom 10020 itunifval 10172 hsmexlem5 10186 axcc2lem 10192 acncc 10196 axcc4dom 10197 domtriomlem 10198 axdclem2 10276 fnct 10293 infinf 10322 unirnfdomd 10323 alephval2 10328 dominfac 10329 iunctb 10330 pwfseqlem4 10418 pwfseqlem5 10419 pwxpndom2 10421 pwdjundom 10423 gchac 10437 wunex2 10494 tskinf 10525 niex 10637 nnexALT 11975 ltweuz 13681 uzenom 13684 nnenom 13700 axdc4uzlem 13703 seqex 13723 rexpen 15937 cctop 22156 2ndcctbss 22606 2ndcdisj 22607 2ndcdisj2 22608 tx2ndc 22802 met2ndci 23678 snct 31048 bnj852 32901 bnj865 32903 satf 33315 satom 33318 satfv0 33320 satfvsuclem1 33321 satfv1lem 33324 satf00 33336 satf0suclem 33337 satf0suc 33338 sat1el2xp 33341 fmla 33343 fmlasuc0 33346 ex-sategoelel 33383 ex-sategoelelomsuc 33388 ex-sategoelel12 33389 prv1n 33393 bj-iomnnom 35430 iunctb2 35574 ctbssinf 35577 finonex 41061 |
Copyright terms: Public domain | W3C validator |