![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > ILE Home > Th. List > peano1 | Structured version 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 3857 | . . . 4 ⊢ ∅ ∈ V | |
2 | 1 | elint 3594 | . . 3 ⊢ (∅ ∈ ∩ {y ∣ (∅ ∈ y ∧ ∀x ∈ y suc x ∈ y)} ↔ ∀z(z ∈ {y ∣ (∅ ∈ y ∧ ∀x ∈ y suc x ∈ y)} → ∅ ∈ z)) |
3 | df-clab 2010 | . . . 4 ⊢ (z ∈ {y ∣ (∅ ∈ y ∧ ∀x ∈ y suc x ∈ y)} ↔ [z / y](∅ ∈ y ∧ ∀x ∈ y suc x ∈ y)) | |
4 | ax-ia1 99 | . . . . . 6 ⊢ ((∅ ∈ y ∧ ∀x ∈ y suc x ∈ y) → ∅ ∈ y) | |
5 | 4 | sbimi 1630 | . . . . 5 ⊢ ([z / y](∅ ∈ y ∧ ∀x ∈ y suc x ∈ y) → [z / y]∅ ∈ y) |
6 | clelsb4 2126 | . . . . 5 ⊢ ([z / y]∅ ∈ y ↔ ∅ ∈ z) | |
7 | 5, 6 | sylib 127 | . . . 4 ⊢ ([z / y](∅ ∈ y ∧ ∀x ∈ y suc x ∈ y) → ∅ ∈ z) |
8 | 3, 7 | sylbi 114 | . . 3 ⊢ (z ∈ {y ∣ (∅ ∈ y ∧ ∀x ∈ y suc x ∈ y)} → ∅ ∈ z) |
9 | 2, 8 | mpgbir 1322 | . 2 ⊢ ∅ ∈ ∩ {y ∣ (∅ ∈ y ∧ ∀x ∈ y suc x ∈ y)} |
10 | dfom3 4240 | . 2 ⊢ 𝜔 = ∩ {y ∣ (∅ ∈ y ∧ ∀x ∈ y suc x ∈ y)} | |
11 | 9, 10 | eleqtrri 2096 | 1 ⊢ ∅ ∈ 𝜔 |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 ∈ wcel 1375 [wsb 1628 {cab 2009 ∀wral 2283 ∅c0 3200 ∩ cint 3588 suc csuc 4049 𝜔com 4238 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-in1 532 ax-in2 533 ax-io 617 ax-5 1316 ax-7 1317 ax-gen 1318 ax-ie1 1364 ax-ie2 1365 ax-8 1377 ax-10 1378 ax-11 1379 ax-i12 1380 ax-bnd 1381 ax-4 1382 ax-17 1401 ax-i9 1405 ax-ial 1410 ax-i5r 1411 ax-ext 2005 ax-nul 3856 |
This theorem depends on definitions: df-bi 110 df-tru 1231 df-nf 1330 df-sb 1629 df-clab 2010 df-cleq 2016 df-clel 2019 df-nfc 2150 df-v 2536 df-dif 2896 df-nul 3201 df-int 3589 df-iom 4239 |
This theorem is referenced by: peano5 4246 limom 4261 nnregexmid 4267 frec0g 5897 frecrdg 5903 oa1suc 5957 nna0r 5967 nnm0r 5968 nnmcl 5970 nnmsucr 5977 1onn 5999 nnm1 6003 nnaordex 6006 nnawordex 6007 1lt2pi 6192 nq0m0r 6297 nq0a0 6298 prarloclem5 6337 peano5set 6509 bj-findeslem0 6528 |
Copyright terms: Public domain | W3C validator |