Theorem peano1 4743

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 4262	. . . 4 ⊢ ∅ ∈ V
2	1	elint 3976	. . 3 ⊢ (∅ ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → ∅ ∈ 𝑧))
3		df-clab 2225	. . . 4 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ [𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦))
4		simpl 109	. . . . . 6 ⊢ ((∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∅ ∈ 𝑦)
5	4	sbimi 1817	. . . . 5 ⊢ ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → [𝑧 / 𝑦]∅ ∈ 𝑦)
6		clelsb2 2344	. . . . 5 ⊢ ([𝑧 / 𝑦]∅ ∈ 𝑦 ↔ ∅ ∈ 𝑧)
7	5, 6	sylib 122	. . . 4 ⊢ ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∅ ∈ 𝑧)
8	3, 7	sylbi 121	. . 3 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → ∅ ∈ 𝑧)
9	2, 8	mpgbir 1506	. 2 ⊢ ∅ ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}
10		dfom3 4741	. 2 ⊢ ω = ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}
11	9, 10	eleqtrri 2314	1 ⊢ ∅ ∈ ω

This proof depends on syntax axioms:   → wi 4   ∧ wa 104  [wsb 1815   ∈ wcel 2209  {cab 2224  ∀wral 2528  ∅c0 3520  ∩ cint 3970  suc csuc 4512  ωcom 4739

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-nul 4261

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-dif 3222  df-nul 3521  df-int 3971  df-iom 4740

This theorem is used by:  peano5  4747  limom  4763  nnregexmid  4770  omsinds  4771  nnpredcl  4772  frec0g  6673  frecabcl  6675  frecrdg  6684  oa1suc  6745  nna0r  6756  nnm0r  6757  nnmcl  6759  nnmsucr  6766  1onn  6798  nnm1  6803  nnaordex  6806  nnawordex  6807  php5  7165  php5dom  7170  0fi  7194  findcard2  7199  findcard2s  7200  infm  7217  inffiexmid  7219  0ct  7453  ctmlemr  7454  ctssdclemn0  7456  ctssdc  7459  omct  7463  nninfisol  7479  fodjum  7492  fodju0  7493  ctssexmid  7496  nninfwlpoimlemg  7521  nninfwlpoimlemginf  7522  1lt2pi  7713  nq0m0r  7829  nq0a0  7830  prarloclem5  7873  frec2uzrand  10862  frecuzrdg0  10870  frecuzrdg0t  10879  frecfzennn  10883  0tonninf  10897  1tonninf  10898  hashinfom  11238  hashunlem  11265  hash1  11273  nninfctlemfo  12841  ennnfonelemj0  13349  ennnfonelem1  13355  ennnfonelemhf1o  13361  ennnfonelemhom  13363  fnpr2o  13718  fvpr0o  13720  xpscf  13726  bj-nn0suc  17212  bj-nn0sucALT  17226  012of  17245  2o01f  17246  pwle2  17250  pwf1oexmid  17251  subctctexmid  17252  peano3nninf  17273  nninfall  17275  nninfsellemdc  17276  nninfsellemeq  17280  nninffeq  17286  nnnninfex  17288  isomninnlem  17302  iswomninnlem  17323  ismkvnnlem  17326