![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > omex | GIF version |
Description: The existence of omega (the class of natural numbers). Axiom 7 of [TakeutiZaring] p. 43. (Contributed by NM, 6-Aug-1994.) |
Ref | Expression |
---|---|
omex | ⊢ ω ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zfinf2 4441 | . . 3 ⊢ ∃𝑦(∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) | |
2 | intexabim 4017 | . . 3 ⊢ (∃𝑦(∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ∈ V) | |
3 | 1, 2 | ax-mp 7 | . 2 ⊢ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ∈ V |
4 | dfom3 4444 | . . 3 ⊢ ω = ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} | |
5 | 4 | eleq1i 2165 | . 2 ⊢ (ω ∈ V ↔ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ∈ V) |
6 | 3, 5 | mpbir 145 | 1 ⊢ ω ∈ V |
Colors of variables: wff set class |
Syntax hints: ∧ wa 103 ∃wex 1436 ∈ wcel 1448 {cab 2086 ∀wral 2375 Vcvv 2641 ∅c0 3310 ∩ cint 3718 suc csuc 4225 ωcom 4442 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 671 ax-5 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-10 1451 ax-11 1452 ax-i12 1453 ax-bndl 1454 ax-4 1455 ax-17 1474 ax-i9 1478 ax-ial 1482 ax-i5r 1483 ax-ext 2082 ax-sep 3986 ax-iinf 4440 |
This theorem depends on definitions: df-bi 116 df-tru 1302 df-nf 1405 df-sb 1704 df-clab 2087 df-cleq 2093 df-clel 2096 df-nfc 2229 df-ral 2380 df-v 2643 df-in 3027 df-ss 3034 df-int 3719 df-iom 4443 |
This theorem is referenced by: peano5 4450 omelon 4460 frecex 6221 frecabex 6225 fict 6691 infnfi 6718 ominf 6719 inffiexmid 6729 omp1eom 6895 difinfsn 6900 0ct 6907 ctmlemr 6908 ctssdclemn0 6910 ctssdclemr 6911 ctssdc 6912 enumct 6914 exmidlpo 6927 infnninf 6934 nnnninf 6935 niex 7021 enq0ex 7148 nq0ex 7149 uzenom 10039 frecfzennn 10040 nnenom 10048 fxnn0nninf 10052 0tonninf 10053 1tonninf 10054 inftonninf 10055 hashinfuni 10364 hashinfom 10365 xpct 11701 ennnfonelemj0 11706 ennnfonelemg 11708 ennnfonelemen 11726 0nninf 12781 nnsf 12783 peano4nninf 12784 peano3nninf 12785 nninfex 12789 nninfself 12793 nninfsellemeq 12794 nninfsellemeqinf 12796 sbthom 12805 |
Copyright terms: Public domain | W3C validator |