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

Theorem peano1 4437
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 3987 . . . 4 ∅ ∈ V
21elint 3716 . . 3 (∅ ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥𝑦 suc 𝑥𝑦)} ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥𝑦 suc 𝑥𝑦)} → ∅ ∈ 𝑧))
3 df-clab 2082 . . . 4 (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥𝑦 suc 𝑥𝑦)} ↔ [𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥𝑦 suc 𝑥𝑦))
4 simpl 108 . . . . . 6 ((∅ ∈ 𝑦 ∧ ∀𝑥𝑦 suc 𝑥𝑦) → ∅ ∈ 𝑦)
54sbimi 1701 . . . . 5 ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥𝑦 suc 𝑥𝑦) → [𝑧 / 𝑦]∅ ∈ 𝑦)
6 clelsb4 2200 . . . . 5 ([𝑧 / 𝑦]∅ ∈ 𝑦 ↔ ∅ ∈ 𝑧)
75, 6sylib 121 . . . 4 ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥𝑦 suc 𝑥𝑦) → ∅ ∈ 𝑧)
83, 7sylbi 120 . . 3 (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥𝑦 suc 𝑥𝑦)} → ∅ ∈ 𝑧)
92, 8mpgbir 1394 . 2 ∅ ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥𝑦 suc 𝑥𝑦)}
10 dfom3 4435 . 2 ω = {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥𝑦 suc 𝑥𝑦)}
119, 10eleqtrri 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