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  6562  frecabcl  6564  frecrdg  6573  oa1suc  6634  nna0r  6645  nnm0r  6646  nnmcl  6648  nnmsucr  6655  1onn  6687  nnm1  6692  nnaordex  6695  nnawordex  6696  php5  7043  php5dom  7048  0fi  7072  findcard2  7077  findcard2s  7078  infm  7095  inffiexmid  7097  0ct  7305  ctmlemr  7306  ctssdclemn0  7308  ctssdc  7311  omct  7315  nninfisol  7331  fodjum  7344  fodju0  7345  ctssexmid  7348  nninfwlpoimlemg  7373  nninfwlpoimlemginf  7374  1lt2pi  7559  nq0m0r  7675  nq0a0  7676  prarloclem5  7719  frec2uzrand  10666  frecuzrdg0  10674  frecuzrdg0t  10683  frecfzennn  10687  0tonninf  10701  1tonninf  10702  hashinfom  11039  hashunlem  11066  hash1  11074  nninfctlemfo  12610  ennnfonelemj0  13021  ennnfonelem1  13027  ennnfonelemhf1o  13033  ennnfonelemhom  13035  fnpr2o  13421  fvpr0o  13423  xpscf  13429  bj-nn0suc  16559  bj-nn0sucALT  16573  012of  16592  2o01f  16593  pwle2  16599  pwf1oexmid  16600  subctctexmid  16601  peano3nninf  16609  nninfall  16611  nninfsellemdc  16612  nninfsellemeq  16616  nninffeq  16622  nnnninfex  16624  isomninnlem  16634  iswomninnlem  16653  ismkvnnlem  16656