![]() |
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 3931 | . . . 4 ⊢ ∅ ∈ V | |
2 | 1 | elint 3668 | . . 3 ⊢ (∅ ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → ∅ ∈ 𝑧)) |
3 | df-clab 2070 | . . . 4 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ [𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)) | |
4 | simpl 107 | . . . . . 6 ⊢ ((∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∅ ∈ 𝑦) | |
5 | 4 | sbimi 1689 | . . . . 5 ⊢ ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → [𝑧 / 𝑦]∅ ∈ 𝑦) |
6 | clelsb4 2188 | . . . . 5 ⊢ ([𝑧 / 𝑦]∅ ∈ 𝑦 ↔ ∅ ∈ 𝑧) | |
7 | 5, 6 | sylib 120 | . . . 4 ⊢ ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∅ ∈ 𝑧) |
8 | 3, 7 | sylbi 119 | . . 3 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → ∅ ∈ 𝑧) |
9 | 2, 8 | mpgbir 1383 | . 2 ⊢ ∅ ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} |
10 | dfom3 4369 | . 2 ⊢ ω = ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} | |
11 | 9, 10 | eleqtrri 2158 | 1 ⊢ ∅ ∈ ω |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ∈ wcel 1434 [wsb 1687 {cab 2069 ∀wral 2353 ∅c0 3269 ∩ cint 3662 suc csuc 4155 ωcom 4367 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 577 ax-in2 578 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2065 ax-nul 3930 |
This theorem depends on definitions: df-bi 115 df-tru 1288 df-nf 1391 df-sb 1688 df-clab 2070 df-cleq 2076 df-clel 2079 df-nfc 2212 df-v 2614 df-dif 2986 df-nul 3270 df-int 3663 df-iom 4368 |
This theorem is referenced by: peano5 4375 limom 4390 nnregexmid 4396 omsinds 4397 frec0g 6093 frecabcl 6095 frecrdg 6104 oa1suc 6159 nna0r 6170 nnm0r 6171 nnmcl 6173 nnmsucr 6180 1onn 6208 nnm1 6212 nnaordex 6215 nnawordex 6216 php5 6503 php5dom 6508 0fin 6529 findcard2 6534 findcard2s 6535 infm 6546 inffiexmid 6548 fodjuomnilemm 6705 fodjuomnilem0 6706 1lt2pi 6801 nq0m0r 6917 nq0a0 6918 prarloclem5 6961 frec2uzrand 9700 frecuzrdg0 9708 frecuzrdg0t 9717 frecfzennn 9721 0tonninf 9733 1tonninf 9734 hashinfom 10020 hashunlem 10046 hash1 10053 bj-nn0suc 11201 bj-nn0sucALT 11215 |
Copyright terms: Public domain | W3C validator |