ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  peano1 GIF version

Theorem peano1 4371
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.)
Assertion
Ref Expression
peano1 ∅ ∈ ω

Proof of Theorem peano1
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0ex 3931 . . . 4 ∅ ∈ V
21elint 3668 . . 3 (∅ ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥𝑦 suc 𝑥𝑦)} ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥𝑦 suc 𝑥𝑦)} → ∅ ∈ 𝑧))
3 df-clab 2070 . . . 4 (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥𝑦 suc 𝑥𝑦)} ↔ [𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥𝑦 suc 𝑥𝑦))
4 simpl 107 . . . . . 6 ((∅ ∈ 𝑦 ∧ ∀𝑥𝑦 suc 𝑥𝑦) → ∅ ∈ 𝑦)
54sbimi 1689 . . . . 5 ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥𝑦 suc 𝑥𝑦) → [𝑧 / 𝑦]∅ ∈ 𝑦)
6 clelsb4 2188 . . . . 5 ([𝑧 / 𝑦]∅ ∈ 𝑦 ↔ ∅ ∈ 𝑧)
75, 6sylib 120 . . . 4 ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥𝑦 suc 𝑥𝑦) → ∅ ∈ 𝑧)
83, 7sylbi 119 . . 3 (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥𝑦 suc 𝑥𝑦)} → ∅ ∈ 𝑧)
92, 8mpgbir 1383 . 2 ∅ ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥𝑦 suc 𝑥𝑦)}
10 dfom3 4369 . 2 ω = {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥𝑦 suc 𝑥𝑦)}
119, 10eleqtrri 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