![]() |
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 4588 | . . 3 ⊢ ∃𝑦(∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) | |
2 | intexabim 4152 | . . 3 ⊢ (∃𝑦(∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ∈ V) | |
3 | 1, 2 | ax-mp 5 | . 2 ⊢ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ∈ V |
4 | dfom3 4591 | . . 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 3844 suc csuc 4365 ωcom 4589 |
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 4121 ax-iinf 4587 |
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 3845 df-iom 4590 |
This theorem is referenced by: peano5 4597 omelon 4608 frecex 6394 frecabex 6398 fict 6867 infnfi 6894 ominf 6895 inffiexmid 6905 omp1eom 7093 difinfsn 7098 0ct 7105 ctmlemr 7106 ctssdclemn0 7108 ctssdclemr 7110 ctssdc 7111 enumct 7113 omct 7115 ctfoex 7116 nninfex 7119 infnninf 7121 infnninfOLD 7122 nnnninf 7123 exmidlpo 7140 nninfdcinf 7168 nninfwlporlem 7170 nninfwlpoimlemg 7172 nninfwlpoim 7175 cc2lem 7264 niex 7310 enq0ex 7437 nq0ex 7438 uzenom 10424 frecfzennn 10425 nnenom 10433 fxnn0nninf 10437 0tonninf 10438 1tonninf 10439 inftonninf 10440 hashinfuni 10756 hashinfom 10757 xpct 12396 ennnfonelemj0 12401 ennnfonelemg 12403 ennnfonelemen 12421 ctiunct 12440 omctfn 12443 ssomct 12445 bj-charfunbi 14533 subctctexmid 14720 0nninf 14723 nnsf 14724 peano4nninf 14725 peano3nninf 14726 nninfself 14732 nninfsellemeq 14733 nninfsellemeqinf 14735 sbthom 14744 |
Copyright terms: Public domain | W3C validator |