Theorem peano1 4690

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 4214	. . . 4 ⊢ ∅ ∈ V
2	1	elint 3932	. . 3 ⊢ (∅ ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → ∅ ∈ 𝑧))
3		df-clab 2216	. . . 4 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ [𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦))
4		simpl 109	. . . . . 6 ⊢ ((∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∅ ∈ 𝑦)
5	4	sbimi 1810	. . . . 5 ⊢ ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → [𝑧 / 𝑦]∅ ∈ 𝑦)
6		clelsb2 2335	. . . . 5 ⊢ ([𝑧 / 𝑦]∅ ∈ 𝑦 ↔ ∅ ∈ 𝑧)
7	5, 6	sylib 122	. . . 4 ⊢ ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∅ ∈ 𝑧)
8	3, 7	sylbi 121	. . 3 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → ∅ ∈ 𝑧)
9	2, 8	mpgbir 1499	. 2 ⊢ ∅ ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}
10		dfom3 4688	. 2 ⊢ ω = ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}
11	9, 10	eleqtrri 2305	1 ⊢ ∅ ∈ ω

Syntax hints:   → wi 4   ∧ wa 104  [wsb 1808   ∈ wcel 2200  {cab 2215  ∀wral 2508  ∅c0 3492  ∩ cint 3926  suc csuc 4460  ωcom 4686

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-nul 4213

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802  df-dif 3200  df-nul 3493  df-int 3927  df-iom 4687

This theorem is referenced by:  peano5  4694  limom  4710  nnregexmid  4717  omsinds  4718  nnpredcl  4719  frec0g  6558  frecabcl  6560  frecrdg  6569  oa1suc  6630  nna0r  6641  nnm0r  6642  nnmcl  6644  nnmsucr  6651  1onn  6683  nnm1  6688  nnaordex  6691  nnawordex  6692  php5  7039  php5dom  7044  0fi  7066  findcard2  7071  findcard2s  7072  infm  7089  inffiexmid  7091  0ct  7297  ctmlemr  7298  ctssdclemn0  7300  ctssdc  7303  omct  7307  nninfisol  7323  fodjum  7336  fodju0  7337  ctssexmid  7340  nninfwlpoimlemg  7365  nninfwlpoimlemginf  7366  1lt2pi  7550  nq0m0r  7666  nq0a0  7667  prarloclem5  7710  frec2uzrand  10657  frecuzrdg0  10665  frecuzrdg0t  10674  frecfzennn  10678  0tonninf  10692  1tonninf  10693  hashinfom  11030  hashunlem  11057  hash1  11065  nninfctlemfo  12601  ennnfonelemj0  13012  ennnfonelem1  13018  ennnfonelemhf1o  13024  ennnfonelemhom  13026  fnpr2o  13412  fvpr0o  13414  xpscf  13420  bj-nn0suc  16495  bj-nn0sucALT  16509  012of  16528  2o01f  16529  pwle2  16535  pwf1oexmid  16536  subctctexmid  16537  peano3nninf  16545  nninfall  16547  nninfsellemdc  16548  nninfsellemeq  16552  nninffeq  16558  nnnninfex  16560  isomninnlem  16570  iswomninnlem  16589  ismkvnnlem  16592