Theorem peano1 4692

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 4216	. . . 4 ⊢ ∅ ∈ V
2	1	elint 3934	. . 3 ⊢ (∅ ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → ∅ ∈ 𝑧))
3		df-clab 2218	. . . 4 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ [𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦))
4		simpl 109	. . . . . 6 ⊢ ((∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∅ ∈ 𝑦)
5	4	sbimi 1812	. . . . 5 ⊢ ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → [𝑧 / 𝑦]∅ ∈ 𝑦)
6		clelsb2 2337	. . . . 5 ⊢ ([𝑧 / 𝑦]∅ ∈ 𝑦 ↔ ∅ ∈ 𝑧)
7	5, 6	sylib 122	. . . 4 ⊢ ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∅ ∈ 𝑧)
8	3, 7	sylbi 121	. . 3 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → ∅ ∈ 𝑧)
9	2, 8	mpgbir 1501	. 2 ⊢ ∅ ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}
10		dfom3 4690	. 2 ⊢ ω = ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}
11	9, 10	eleqtrri 2307	1 ⊢ ∅ ∈ ω

Syntax hints:   → wi 4   ∧ wa 104  [wsb 1810   ∈ wcel 2202  {cab 2217  ∀wral 2510  ∅c0 3494  ∩ cint 3928  suc csuc 4462  ωcom 4688

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 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-nul 4215

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-dif 3202  df-nul 3495  df-int 3929  df-iom 4689

This theorem is referenced by:  peano5  4696  limom  4712  nnregexmid  4719  omsinds  4720  nnpredcl  4721  frec0g  6563  frecabcl  6565  frecrdg  6574  oa1suc  6635  nna0r  6646  nnm0r  6647  nnmcl  6649  nnmsucr  6656  1onn  6688  nnm1  6693  nnaordex  6696  nnawordex  6697  php5  7044  php5dom  7049  0fi  7073  findcard2  7078  findcard2s  7079  infm  7096  inffiexmid  7098  0ct  7306  ctmlemr  7307  ctssdclemn0  7309  ctssdc  7312  omct  7316  nninfisol  7332  fodjum  7345  fodju0  7346  ctssexmid  7349  nninfwlpoimlemg  7374  nninfwlpoimlemginf  7375  1lt2pi  7560  nq0m0r  7676  nq0a0  7677  prarloclem5  7720  frec2uzrand  10668  frecuzrdg0  10676  frecuzrdg0t  10685  frecfzennn  10689  0tonninf  10703  1tonninf  10704  hashinfom  11041  hashunlem  11068  hash1  11076  nninfctlemfo  12629  ennnfonelemj0  13040  ennnfonelem1  13046  ennnfonelemhf1o  13052  ennnfonelemhom  13054  fnpr2o  13440  fvpr0o  13442  xpscf  13448  bj-nn0suc  16610  bj-nn0sucALT  16624  012of  16643  2o01f  16644  pwle2  16650  pwf1oexmid  16651  subctctexmid  16652  peano3nninf  16660  nninfall  16662  nninfsellemdc  16663  nninfsellemeq  16667  nninffeq  16673  nnnninfex  16675  isomninnlem  16685  iswomninnlem  16705  ismkvnnlem  16708