![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > peano1 | GIF version |
Description: Zero is a natural number. One of Peano's five postulates for arithmetic. Proposition 7.30(1) of [TakeutiZaring] p. 42. (Contributed by NM, 15-May-1994.) |
Ref | Expression |
---|---|
peano1 | ⊢ ∅ ∈ ω |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0ex 4145 | . . . 4 ⊢ ∅ ∈ V | |
2 | 1 | elint 3865 | . . 3 ⊢ (∅ ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → ∅ ∈ 𝑧)) |
3 | df-clab 2176 | . . . 4 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ [𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)) | |
4 | simpl 109 | . . . . . 6 ⊢ ((∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∅ ∈ 𝑦) | |
5 | 4 | sbimi 1775 | . . . . 5 ⊢ ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → [𝑧 / 𝑦]∅ ∈ 𝑦) |
6 | clelsb2 2295 | . . . . 5 ⊢ ([𝑧 / 𝑦]∅ ∈ 𝑦 ↔ ∅ ∈ 𝑧) | |
7 | 5, 6 | sylib 122 | . . . 4 ⊢ ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∅ ∈ 𝑧) |
8 | 3, 7 | sylbi 121 | . . 3 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → ∅ ∈ 𝑧) |
9 | 2, 8 | mpgbir 1464 | . 2 ⊢ ∅ ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} |
10 | dfom3 4609 | . 2 ⊢ ω = ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} | |
11 | 9, 10 | eleqtrri 2265 | 1 ⊢ ∅ ∈ ω |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 [wsb 1773 ∈ wcel 2160 {cab 2175 ∀wral 2468 ∅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-in1 615 ax-in2 616 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-nul 4144 |
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-v 2754 df-dif 3146 df-nul 3438 df-int 3860 df-iom 4608 |
This theorem is referenced by: peano5 4615 limom 4631 nnregexmid 4638 omsinds 4639 nnpredcl 4640 frec0g 6422 frecabcl 6424 frecrdg 6433 oa1suc 6492 nna0r 6503 nnm0r 6504 nnmcl 6506 nnmsucr 6513 1onn 6545 nnm1 6550 nnaordex 6553 nnawordex 6554 php5 6886 php5dom 6891 0fin 6912 findcard2 6917 findcard2s 6918 infm 6932 inffiexmid 6934 0ct 7136 ctmlemr 7137 ctssdclemn0 7139 ctssdc 7142 omct 7146 nninfisol 7161 fodjum 7174 fodju0 7175 ctssexmid 7178 nninfwlpoimlemg 7203 nninfwlpoimlemginf 7204 1lt2pi 7369 nq0m0r 7485 nq0a0 7486 prarloclem5 7529 frec2uzrand 10436 frecuzrdg0 10444 frecuzrdg0t 10453 frecfzennn 10457 0tonninf 10470 1tonninf 10471 hashinfom 10790 hashunlem 10816 hash1 10823 ennnfonelemj0 12452 ennnfonelem1 12458 ennnfonelemhf1o 12464 ennnfonelemhom 12466 fnpr2o 12815 fvpr0o 12817 xpscf 12823 bj-nn0suc 15174 bj-nn0sucALT 15188 012of 15204 2o01f 15205 pwle2 15207 pwf1oexmid 15208 subctctexmid 15209 peano3nninf 15215 nninfall 15217 nninfsellemdc 15218 nninfsellemeq 15222 nninffeq 15228 isomninnlem 15237 iswomninnlem 15256 ismkvnnlem 15259 |
Copyright terms: Public domain | W3C validator |