![]() |
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 4606 | . . 3 ⊢ ∃𝑦(∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) | |
2 | intexabim 4170 | . . 3 ⊢ (∃𝑦(∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ∈ V) | |
3 | 1, 2 | ax-mp 5 | . 2 ⊢ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ∈ V |
4 | dfom3 4609 | . . 3 ⊢ ω = ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} | |
5 | 4 | eleq1i 2255 | . 2 ⊢ (ω ∈ V ↔ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ∈ V) |
6 | 3, 5 | mpbir 146 | 1 ⊢ ω ∈ V |
Colors of variables: wff set class |
Syntax hints: ∧ wa 104 ∃wex 1503 ∈ wcel 2160 {cab 2175 ∀wral 2468 Vcvv 2752 ∅c0 3437 ∩ cint 3859 suc csuc 4383 ωcom 4607 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 ax-sep 4136 ax-iinf 4605 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ral 2473 df-v 2754 df-in 3150 df-ss 3157 df-int 3860 df-iom 4608 |
This theorem is referenced by: peano5 4615 omelon 4626 frecex 6419 frecabex 6423 fict 6896 infnfi 6923 ominf 6924 inffiexmid 6934 omp1eom 7124 difinfsn 7129 0ct 7136 ctmlemr 7137 ctssdclemn0 7139 ctssdclemr 7141 ctssdc 7142 enumct 7144 omct 7146 ctfoex 7147 nninfex 7150 infnninf 7152 infnninfOLD 7153 nnnninf 7154 exmidlpo 7171 nninfdcinf 7199 nninfwlporlem 7201 nninfwlpoimlemg 7203 nninfwlpoim 7206 cc2lem 7295 niex 7341 enq0ex 7468 nq0ex 7469 uzenom 10456 frecfzennn 10457 nnenom 10465 fxnn0nninf 10469 0tonninf 10470 1tonninf 10471 inftonninf 10472 hashinfuni 10789 hashinfom 10790 xpct 12447 ennnfonelemj0 12452 ennnfonelemg 12454 ennnfonelemen 12472 ctiunct 12491 omctfn 12494 ssomct 12496 bj-charfunbi 15024 subctctexmid 15212 0nninf 15215 nnsf 15216 peano4nninf 15217 peano3nninf 15218 nninfself 15224 nninfsellemeq 15225 nninfsellemeqinf 15227 sbthom 15236 |
Copyright terms: Public domain | W3C validator |