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  7426  nq0m0r  7542  nq0a0  7543  prarloclem5  7586  frec2uzrand  10516  frecuzrdg0  10524  frecuzrdg0t  10533  frecfzennn  10537  0tonninf  10551  1tonninf  10552  hashinfom  10889  hashunlem  10915  hash1  10922  nninfctlemfo  12234  ennnfonelemj0  12645  ennnfonelem1  12651  ennnfonelemhf1o  12657  ennnfonelemhom  12659  fnpr2o  13043  fvpr0o  13045  xpscf  13051  bj-nn0suc  15718  bj-nn0sucALT  15732  012of  15748  2o01f  15749  pwle2  15753  pwf1oexmid  15754  subctctexmid  15755  peano3nninf  15762  nninfall  15764  nninfsellemdc  15765  nninfsellemeq  15769  nninffeq  15775  nnnninfex  15777  isomninnlem  15787  iswomninnlem  15806  ismkvnnlem  15809