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.

Step	Hyp	Ref	Expression
1		0ex 3856	. . . 4 ⊢ ∅ ∈ V
2	1	elint 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)
5	4	sbimi 1629	. . . . 5 ⊢ ([z / y](∅ ∈ y ∧ ∀x ∈ y suc x ∈ y) → [z / y]∅ ∈ y)
6		clelsb4 2125	. . . . 5 ⊢ ([z / y]∅ ∈ y ↔ ∅ ∈ z)
7	5, 6	sylib 127	. . . 4 ⊢ ([z / y](∅ ∈ y ∧ ∀x ∈ y suc x ∈ y) → ∅ ∈ z)
8	3, 7	sylbi 114	. . 3 ⊢ (z ∈ {y ∣ (∅ ∈ y ∧ ∀x ∈ y suc x ∈ y)} → ∅ ∈ z)
9	2, 8	mpgbir 1322	. 2 ⊢ ∅ ∈ ∩ {y ∣ (∅ ∈ y ∧ ∀x ∈ y suc x ∈ y)}
10		dfom3 4240	. 2 ⊢ 𝜔 = ∩ {y ∣ (∅ ∈ y ∧ ∀x ∈ y suc x ∈ y)}
11	9, 10	eleqtrri 2095	1 ⊢ ∅ ∈ 𝜔

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