Theorem peano1 4698

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 4221	. . . 4 ⊢ ∅ ∈ V
2	1	elint 3939	. . 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 1502	. 2 ⊢ ∅ ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}
10		dfom3 4696	. 2 ⊢ ω = ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}
11	9, 10	eleqtrri 2307	1 ⊢ ∅ ∈ ω

Syntax hints:   → wi 4   ∧ wa 104  [wsb 1810   ∈ wcel 2202  {cab 2217  ∀wral 2511  ∅c0 3496  ∩ cint 3933  suc csuc 4468  ωcom 4694

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-nul 4220

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-dif 3203  df-nul 3497  df-int 3934  df-iom 4695

This theorem is referenced by:  peano5  4702  limom  4718  nnregexmid  4725  omsinds  4726  nnpredcl  4727  frec0g  6606  frecabcl  6608  frecrdg  6617  oa1suc  6678  nna0r  6689  nnm0r  6690  nnmcl  6692  nnmsucr  6699  1onn  6731  nnm1  6736  nnaordex  6739  nnawordex  6740  php5  7087  php5dom  7092  0fi  7116  findcard2  7121  findcard2s  7122  infm  7139  inffiexmid  7141  0ct  7349  ctmlemr  7350  ctssdclemn0  7352  ctssdc  7355  omct  7359  nninfisol  7375  fodjum  7388  fodju0  7389  ctssexmid  7392  nninfwlpoimlemg  7417  nninfwlpoimlemginf  7418  1lt2pi  7603  nq0m0r  7719  nq0a0  7720  prarloclem5  7763  frec2uzrand  10713  frecuzrdg0  10721  frecuzrdg0t  10730  frecfzennn  10734  0tonninf  10748  1tonninf  10749  hashinfom  11086  hashunlem  11113  hash1  11121  nninfctlemfo  12674  ennnfonelemj0  13085  ennnfonelem1  13091  ennnfonelemhf1o  13097  ennnfonelemhom  13099  fnpr2o  13485  fvpr0o  13487  xpscf  13493  bj-nn0suc  16663  bj-nn0sucALT  16677  012of  16696  2o01f  16697  pwle2  16703  pwf1oexmid  16704  subctctexmid  16705  peano3nninf  16716  nninfall  16718  nninfsellemdc  16719  nninfsellemeq  16723  nninffeq  16729  nnnninfex  16731  isomninnlem  16745  iswomninnlem  16765  ismkvnnlem  16768