![]() |
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 4589 | . . 3 ⊢ ∃𝑦(∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) | |
2 | intexabim 4153 | . . 3 ⊢ (∃𝑦(∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ∈ V) | |
3 | 1, 2 | ax-mp 5 | . 2 ⊢ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ∈ V |
4 | dfom3 4592 | . . 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 2738 ∅c0 3423 ∩ cint 3845 suc csuc 4366 ωcom 4590 |
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 4122 ax-iinf 4588 |
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 2740 df-in 3136 df-ss 3143 df-int 3846 df-iom 4591 |
This theorem is referenced by: peano5 4598 omelon 4609 frecex 6395 frecabex 6399 fict 6868 infnfi 6895 ominf 6896 inffiexmid 6906 omp1eom 7094 difinfsn 7099 0ct 7106 ctmlemr 7107 ctssdclemn0 7109 ctssdclemr 7111 ctssdc 7112 enumct 7114 omct 7116 ctfoex 7117 nninfex 7120 infnninf 7122 infnninfOLD 7123 nnnninf 7124 exmidlpo 7141 nninfdcinf 7169 nninfwlporlem 7171 nninfwlpoimlemg 7173 nninfwlpoim 7176 cc2lem 7265 niex 7311 enq0ex 7438 nq0ex 7439 uzenom 10425 frecfzennn 10426 nnenom 10434 fxnn0nninf 10438 0tonninf 10439 1tonninf 10440 inftonninf 10441 hashinfuni 10757 hashinfom 10758 xpct 12397 ennnfonelemj0 12402 ennnfonelemg 12404 ennnfonelemen 12422 ctiunct 12441 omctfn 12444 ssomct 12446 bj-charfunbi 14566 subctctexmid 14753 0nninf 14756 nnsf 14757 peano4nninf 14758 peano3nninf 14759 nninfself 14765 nninfsellemeq 14766 nninfsellemeqinf 14768 sbthom 14777 |
Copyright terms: Public domain | W3C validator |