![]() |
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 3987 | . . . 4 ⊢ ∅ ∈ V | |
2 | 1 | elint 3716 | . . 3 ⊢ (∅ ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → ∅ ∈ 𝑧)) |
3 | df-clab 2082 | . . . 4 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ [𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)) | |
4 | simpl 108 | . . . . . 6 ⊢ ((∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∅ ∈ 𝑦) | |
5 | 4 | sbimi 1701 | . . . . 5 ⊢ ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → [𝑧 / 𝑦]∅ ∈ 𝑦) |
6 | clelsb4 2200 | . . . . 5 ⊢ ([𝑧 / 𝑦]∅ ∈ 𝑦 ↔ ∅ ∈ 𝑧) | |
7 | 5, 6 | sylib 121 | . . . 4 ⊢ ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∅ ∈ 𝑧) |
8 | 3, 7 | sylbi 120 | . . 3 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → ∅ ∈ 𝑧) |
9 | 2, 8 | mpgbir 1394 | . 2 ⊢ ∅ ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} |
10 | dfom3 4435 | . 2 ⊢ ω = ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} | |
11 | 9, 10 | eleqtrri 2170 | 1 ⊢ ∅ ∈ ω |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∈ wcel 1445 [wsb 1699 {cab 2081 ∀wral 2370 ∅c0 3302 ∩ cint 3710 suc csuc 4216 ωcom 4433 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 582 ax-in2 583 ax-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 ax-nul 3986 |
This theorem depends on definitions: df-bi 116 df-tru 1299 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-v 2635 df-dif 3015 df-nul 3303 df-int 3711 df-iom 4434 |
This theorem is referenced by: peano5 4441 limom 4456 nnregexmid 4462 omsinds 4463 nnpredcl 4464 frec0g 6200 frecabcl 6202 frecrdg 6211 oa1suc 6268 nna0r 6279 nnm0r 6280 nnmcl 6282 nnmsucr 6289 1onn 6319 nnm1 6323 nnaordex 6326 nnawordex 6327 php5 6654 php5dom 6659 0fin 6680 findcard2 6685 findcard2s 6686 infm 6700 inffiexmid 6702 0ct 6869 ctmlemr 6870 fodjum 6889 fodju0 6890 1lt2pi 6996 nq0m0r 7112 nq0a0 7113 prarloclem5 7156 frec2uzrand 9961 frecuzrdg0 9969 frecuzrdg0t 9978 frecfzennn 9982 0tonninf 9994 1tonninf 9995 hashinfom 10317 hashunlem 10343 hash1 10350 bj-nn0suc 12583 bj-nn0sucALT 12597 peano3nninf 12618 nninfall 12621 nninfsellemdc 12623 nninfsellemeq 12627 |
Copyright terms: Public domain | W3C validator |