Theorem peano1 4631

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 4161	. . . 4 ⊢ ∅ ∈ V
2	1	elint 3881	. . 3 ⊢ (∅ ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → ∅ ∈ 𝑧))
3		df-clab 2183	. . . 4 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ [𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦))
4		simpl 109	. . . . . 6 ⊢ ((∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∅ ∈ 𝑦)
5	4	sbimi 1778	. . . . 5 ⊢ ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → [𝑧 / 𝑦]∅ ∈ 𝑦)
6		clelsb2 2302	. . . . 5 ⊢ ([𝑧 / 𝑦]∅ ∈ 𝑦 ↔ ∅ ∈ 𝑧)
7	5, 6	sylib 122	. . . 4 ⊢ ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∅ ∈ 𝑧)
8	3, 7	sylbi 121	. . 3 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → ∅ ∈ 𝑧)
9	2, 8	mpgbir 1467	. 2 ⊢ ∅ ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}
10		dfom3 4629	. 2 ⊢ ω = ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}
11	9, 10	eleqtrri 2272	1 ⊢ ∅ ∈ ω

Syntax hints:   → wi 4   ∧ wa 104  [wsb 1776   ∈ wcel 2167  {cab 2182  ∀wral 2475  ∅c0 3451  ∩ cint 3875  suc csuc 4401  ωcom 4627

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 615  ax-in2 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-nul 4160

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-dif 3159  df-nul 3452  df-int 3876  df-iom 4628

This theorem is referenced by:  peano5  4635  limom  4651  nnregexmid  4658  omsinds  4659  nnpredcl  4660  frec0g  6464  frecabcl  6466  frecrdg  6475  oa1suc  6534  nna0r  6545  nnm0r  6546  nnmcl  6548  nnmsucr  6555  1onn  6587  nnm1  6592  nnaordex  6595  nnawordex  6596  php5  6928  php5dom  6933  0fin  6954  findcard2  6959  findcard2s  6960  infm  6974  inffiexmid  6976  0ct  7182  ctmlemr  7183  ctssdclemn0  7185  ctssdc  7188  omct  7192  nninfisol  7208  fodjum  7221  fodju0  7222  ctssexmid  7225  nninfwlpoimlemg  7250  nninfwlpoimlemginf  7251  1lt2pi  7424  nq0m0r  7540  nq0a0  7541  prarloclem5  7584  frec2uzrand  10514  frecuzrdg0  10522  frecuzrdg0t  10531  frecfzennn  10535  0tonninf  10549  1tonninf  10550  hashinfom  10887  hashunlem  10913  hash1  10920  nninfctlemfo  12232  ennnfonelemj0  12643  ennnfonelem1  12649  ennnfonelemhf1o  12655  ennnfonelemhom  12657  fnpr2o  13041  fvpr0o  13043  xpscf  13049  bj-nn0suc  15694  bj-nn0sucALT  15708  012of  15724  2o01f  15725  pwle2  15729  pwf1oexmid  15730  subctctexmid  15731  peano3nninf  15738  nninfall  15740  nninfsellemdc  15741  nninfsellemeq  15745  nninffeq  15751  isomninnlem  15761  iswomninnlem  15780  ismkvnnlem  15783