Theorem peano1 4213

Description: Zero is a natural number. One of Peano's 5 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 3836	. . . 4 ⊢ ∅ ∈ V
2	1	elint 3573	. . 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 1321	. 2 ⊢ ∅ ∈ ∩ {y ∣ (∅ ∈ y ∧ ∀x ∈ y suc x ∈ y)}
10		dfom3 4211	. 2 ⊢ 𝜔 = ∩ {y ∣ (∅ ∈ y ∧ ∀x ∈ y suc x ∈ y)}
11	9, 10	eleqtrri 2095	1 ⊢ ∅ ∈ 𝜔

Syntax hints:   → wi 4   ∧ wa 97   ∈ wcel 1375  [wsb 1627  {cab 2008  ∀wral 2282  ∅c0 3202  ∩ cint 3567  suc csuc 4026  𝜔com 4209

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 1315  ax-7 1316  ax-gen 1317  ax-ie1 1362  ax-ie2 1363  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 2004  ax-nul 3835

This theorem depends on definitions:  df-bi 110  df-tru 1231  df-nf 1329  df-sb 1628  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-v 2535  df-dif 2898  df-nul 3203  df-int 3568  df-iom 4210

This theorem is referenced by:  peano5  4217  limom  4232  frec0g  5868