![]() |
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 4586 | . . 3 ⊢ ∃𝑦(∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) | |
2 | intexabim 4150 | . . 3 ⊢ (∃𝑦(∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ∈ V) | |
3 | 1, 2 | ax-mp 5 | . 2 ⊢ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ∈ V |
4 | dfom3 4589 | . . 3 ⊢ ω = ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} | |
5 | 4 | eleq1i 2243 | . 2 ⊢ (ω ∈ V ↔ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ∈ V) |
6 | 3, 5 | mpbir 146 | 1 ⊢ ω ∈ V |
Colors of variables: wff set class |
Syntax hints: ∧ wa 104 ∃wex 1492 ∈ wcel 2148 {cab 2163 ∀wral 2455 Vcvv 2737 ∅c0 3422 ∩ cint 3843 suc csuc 4363 ωcom 4587 |
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 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 ax-sep 4119 ax-iinf 4585 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ral 2460 df-v 2739 df-in 3135 df-ss 3142 df-int 3844 df-iom 4588 |
This theorem is referenced by: peano5 4595 omelon 4606 frecex 6390 frecabex 6394 fict 6863 infnfi 6890 ominf 6891 inffiexmid 6901 omp1eom 7089 difinfsn 7094 0ct 7101 ctmlemr 7102 ctssdclemn0 7104 ctssdclemr 7106 ctssdc 7107 enumct 7109 omct 7111 ctfoex 7112 nninfex 7115 infnninf 7117 infnninfOLD 7118 nnnninf 7119 exmidlpo 7136 nninfdcinf 7164 nninfwlporlem 7166 nninfwlpoimlemg 7168 nninfwlpoim 7171 cc2lem 7260 niex 7306 enq0ex 7433 nq0ex 7434 uzenom 10418 frecfzennn 10419 nnenom 10427 fxnn0nninf 10431 0tonninf 10432 1tonninf 10433 inftonninf 10434 hashinfuni 10748 hashinfom 10749 xpct 12387 ennnfonelemj0 12392 ennnfonelemg 12394 ennnfonelemen 12412 ctiunct 12431 omctfn 12434 ssomct 12436 bj-charfunbi 14334 subctctexmid 14521 0nninf 14524 nnsf 14525 peano4nninf 14526 peano3nninf 14527 nninfself 14533 nninfsellemeq 14534 nninfsellemeqinf 14536 sbthom 14545 |
Copyright terms: Public domain | W3C validator |