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 3856 . . . 4 V
21elint 3593 . . 3 (∅ {y ∣ (∅ y x y suc x y)} ↔ z(z {y ∣ (∅ y x y suc x y)} → ∅ z))
3 df-clab 2009 . . . 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 1629 . . . . 5 ([z / y](∅ y x y suc x y) → [z / y]∅ y)
6 clelsb4 2125 . . . . 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 2095 1 𝜔
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   wcel 1374  [wsb 1627  {cab 2008  wral 2282  c0 3199   cint 3587  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 1363  ax-ie2 1364  ax-8 1376  ax-10 1377  ax-11 1378  ax-i12 1379  ax-bnd 1380  ax-4 1381  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004  ax-nul 3855
This theorem depends on definitions:  df-bi 110  df-tru 1231  df-nf 1330  df-sb 1628  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-v 2535  df-dif 2895  df-nul 3200  df-int 3588  df-iom 4239
This theorem is referenced by:  peano5  4246  limom  4261  nnregexmid  4267  frec0g  5900  frecrdg  5906  oa1suc  5960  nna0r  5970  nnm0r  5971  nnmcl  5973  nnmsucr  5980  1onn  6002  nnm1  6006  nnaordex  6009  nnawordex  6010  1lt2pi  6198  nq0m0r  6309  nq0a0  6310  prarloclem5  6352  peano5set  6841  bj-nn0suc  6861  bj-nn0sucALT  6875
  Copyright terms: Public domain W3C validator