Theorem peano1 4630

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 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		0ex 4160	. . . 4 ⊢ ∅ ∈ V
2	1	elint 3880	. . 3 ⊢ (∅ ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → ∅ ∈ 𝑧))
3		df-clab 2183	. . . 4 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ [𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦))
4		simpl 109	. . . . . 6 ⊢ ((∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∅ ∈ 𝑦)
5	4	sbimi 1778	. . . . 5 ⊢ ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → [𝑧 / 𝑦]∅ ∈ 𝑦)
6		clelsb2 2302	. . . . 5 ⊢ ([𝑧 / 𝑦]∅ ∈ 𝑦 ↔ ∅ ∈ 𝑧)
7	5, 6	sylib 122	. . . 4 ⊢ ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∅ ∈ 𝑧)
8	3, 7	sylbi 121	. . 3 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → ∅ ∈ 𝑧)
9	2, 8	mpgbir 1467	. 2 ⊢ ∅ ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}
10		dfom3 4628	. 2 ⊢ ω = ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}
11	9, 10	eleqtrri 2272	1 ⊢ ∅ ∈ ω

Syntax hints:   → wi 4   ∧ wa 104  [wsb 1776   ∈ wcel 2167  {cab 2182  ∀wral 2475  ∅c0 3450  ∩ cint 3874  suc csuc 4400  ωcom 4626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-nul 4159

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-dif 3159  df-nul 3451  df-int 3875  df-iom 4627

This theorem is referenced by:  peano5  4634  limom  4650  nnregexmid  4657  omsinds  4658  nnpredcl  4659  frec0g  6455  frecabcl  6457  frecrdg  6466  oa1suc  6525  nna0r  6536  nnm0r  6537  nnmcl  6539  nnmsucr  6546  1onn  6578  nnm1  6583  nnaordex  6586  nnawordex  6587  php5  6919  php5dom  6924  0fin  6945  findcard2  6950  findcard2s  6951  infm  6965  inffiexmid  6967  0ct  7173  ctmlemr  7174  ctssdclemn0  7176  ctssdc  7179  omct  7183  nninfisol  7199  fodjum  7212  fodju0  7213  ctssexmid  7216  nninfwlpoimlemg  7241  nninfwlpoimlemginf  7242  1lt2pi  7407  nq0m0r  7523  nq0a0  7524  prarloclem5  7567  frec2uzrand  10497  frecuzrdg0  10505  frecuzrdg0t  10514  frecfzennn  10518  0tonninf  10532  1tonninf  10533  hashinfom  10870  hashunlem  10896  hash1  10903  nninfctlemfo  12207  ennnfonelemj0  12618  ennnfonelem1  12624  ennnfonelemhf1o  12630  ennnfonelemhom  12632  fnpr2o  12982  fvpr0o  12984  xpscf  12990  bj-nn0suc  15610  bj-nn0sucALT  15624  012of  15640  2o01f  15641  pwle2  15643  pwf1oexmid  15644  subctctexmid  15645  peano3nninf  15651  nninfall  15653  nninfsellemdc  15654  nninfsellemeq  15658  nninffeq  15664  isomninnlem  15674  iswomninnlem  15693  ismkvnnlem  15696