Theorem peano1 4571

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 4109	. . . 4 ⊢ ∅ ∈ V
2	1	elint 3830	. . 3 ⊢ (∅ ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → ∅ ∈ 𝑧))
3		df-clab 2152	. . . 4 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ [𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦))
4		simpl 108	. . . . . 6 ⊢ ((∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∅ ∈ 𝑦)
5	4	sbimi 1752	. . . . 5 ⊢ ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → [𝑧 / 𝑦]∅ ∈ 𝑦)
6		clelsb2 2272	. . . . 5 ⊢ ([𝑧 / 𝑦]∅ ∈ 𝑦 ↔ ∅ ∈ 𝑧)
7	5, 6	sylib 121	. . . 4 ⊢ ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∅ ∈ 𝑧)
8	3, 7	sylbi 120	. . 3 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → ∅ ∈ 𝑧)
9	2, 8	mpgbir 1441	. 2 ⊢ ∅ ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}
10		dfom3 4569	. 2 ⊢ ω = ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}
11	9, 10	eleqtrri 2242	1 ⊢ ∅ ∈ ω

Syntax hints:   → wi 4   ∧ wa 103  [wsb 1750   ∈ wcel 2136  {cab 2151  ∀wral 2444  ∅c0 3409  ∩ cint 3824  suc csuc 4343  ωcom 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147  ax-nul 4108

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-v 2728  df-dif 3118  df-nul 3410  df-int 3825  df-iom 4568

This theorem is referenced by:  peano5  4575  limom  4591  nnregexmid  4598  omsinds  4599  nnpredcl  4600  frec0g  6365  frecabcl  6367  frecrdg  6376  oa1suc  6435  nna0r  6446  nnm0r  6447  nnmcl  6449  nnmsucr  6456  1onn  6488  nnm1  6492  nnaordex  6495  nnawordex  6496  php5  6824  php5dom  6829  0fin  6850  findcard2  6855  findcard2s  6856  infm  6870  inffiexmid  6872  0ct  7072  ctmlemr  7073  ctssdclemn0  7075  ctssdc  7078  omct  7082  nninfisol  7097  fodjum  7110  fodju0  7111  ctssexmid  7114  1lt2pi  7281  nq0m0r  7397  nq0a0  7398  prarloclem5  7441  frec2uzrand  10340  frecuzrdg0  10348  frecuzrdg0t  10357  frecfzennn  10361  0tonninf  10374  1tonninf  10375  hashinfom  10691  hashunlem  10717  hash1  10724  ennnfonelemj0  12334  ennnfonelem1  12340  ennnfonelemhf1o  12346  ennnfonelemhom  12348  bj-nn0suc  13846  bj-nn0sucALT  13860  012of  13875  2o01f  13876  pwle2  13878  pwf1oexmid  13879  subctctexmid  13881  peano3nninf  13887  nninfall  13889  nninfsellemdc  13890  nninfsellemeq  13894  nninffeq  13900  isomninnlem  13909  iswomninnlem  13928  ismkvnnlem  13931