Theorem peano1 4686

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 4211	. . . 4 ⊢ ∅ ∈ V
2	1	elint 3929	. . 3 ⊢ (∅ ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → ∅ ∈ 𝑧))
3		df-clab 2216	. . . 4 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ [𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦))
4		simpl 109	. . . . . 6 ⊢ ((∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∅ ∈ 𝑦)
5	4	sbimi 1810	. . . . 5 ⊢ ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → [𝑧 / 𝑦]∅ ∈ 𝑦)
6		clelsb2 2335	. . . . 5 ⊢ ([𝑧 / 𝑦]∅ ∈ 𝑦 ↔ ∅ ∈ 𝑧)
7	5, 6	sylib 122	. . . 4 ⊢ ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∅ ∈ 𝑧)
8	3, 7	sylbi 121	. . 3 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → ∅ ∈ 𝑧)
9	2, 8	mpgbir 1499	. 2 ⊢ ∅ ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}
10		dfom3 4684	. 2 ⊢ ω = ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}
11	9, 10	eleqtrri 2305	1 ⊢ ∅ ∈ ω

Syntax hints:   → wi 4   ∧ wa 104  [wsb 1808   ∈ wcel 2200  {cab 2215  ∀wral 2508  ∅c0 3491  ∩ cint 3923  suc csuc 4456  ωcom 4682

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-nul 4210

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-dif 3199  df-nul 3492  df-int 3924  df-iom 4683

This theorem is referenced by:  peano5  4690  limom  4706  nnregexmid  4713  omsinds  4714  nnpredcl  4715  frec0g  6549  frecabcl  6551  frecrdg  6560  oa1suc  6621  nna0r  6632  nnm0r  6633  nnmcl  6635  nnmsucr  6642  1onn  6674  nnm1  6679  nnaordex  6682  nnawordex  6683  php5  7027  php5dom  7032  0fi  7054  findcard2  7059  findcard2s  7060  infm  7077  inffiexmid  7079  0ct  7285  ctmlemr  7286  ctssdclemn0  7288  ctssdc  7291  omct  7295  nninfisol  7311  fodjum  7324  fodju0  7325  ctssexmid  7328  nninfwlpoimlemg  7353  nninfwlpoimlemginf  7354  1lt2pi  7538  nq0m0r  7654  nq0a0  7655  prarloclem5  7698  frec2uzrand  10639  frecuzrdg0  10647  frecuzrdg0t  10656  frecfzennn  10660  0tonninf  10674  1tonninf  10675  hashinfom  11012  hashunlem  11038  hash1  11046  nninfctlemfo  12576  ennnfonelemj0  12987  ennnfonelem1  12993  ennnfonelemhf1o  12999  ennnfonelemhom  13001  fnpr2o  13387  fvpr0o  13389  xpscf  13395  bj-nn0suc  16382  bj-nn0sucALT  16396  012of  16416  2o01f  16417  pwle2  16423  pwf1oexmid  16424  subctctexmid  16425  peano3nninf  16433  nninfall  16435  nninfsellemdc  16436  nninfsellemeq  16440  nninffeq  16446  nnnninfex  16448  isomninnlem  16458  iswomninnlem  16477  ismkvnnlem  16480