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 3857	. . . 4 ⊢ ∅ ∈ V
2	1	elint 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)
5	4	sbimi 1630	. . . . 5 ⊢ ([z / y](∅ ∈ y ∧ ∀x ∈ y suc x ∈ y) → [z / y]∅ ∈ y)
6		clelsb4 2126	. . . . 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 2096	1 ⊢ ∅ ∈ 𝜔

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