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

Theorem peano1 4242
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 x y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0ex 3857 . . . 4 V
21elint 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)
54sbimi 1630 . . . . 5 ([z / y](∅ y x y suc x y) → [z / y]∅ y)
6 clelsb4 2126 . . . . 5 ([z / y]∅ y ↔ ∅ z)
75, 6sylib 127 . . . 4 ([z / y](∅ y x y suc x y) → ∅ z)
83, 7sylbi 114 . . 3 (z {y ∣ (∅ y x y suc x y)} → ∅ z)
92, 8mpgbir 1322 . 2 {y ∣ (∅ y x y suc x y)}
10 dfom3 4240 . 2 𝜔 = {y ∣ (∅ y x y suc x y)}
119, 10eleqtrri 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