Theorem peano1 4626

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 4156	. . . 4 ⊢ ∅ ∈ V
2	1	elint 3876	. . 3 ⊢ (∅ ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → ∅ ∈ 𝑧))
3		df-clab 2180	. . . 4 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ [𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦))
4		simpl 109	. . . . . 6 ⊢ ((∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∅ ∈ 𝑦)
5	4	sbimi 1775	. . . . 5 ⊢ ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → [𝑧 / 𝑦]∅ ∈ 𝑦)
6		clelsb2 2299	. . . . 5 ⊢ ([𝑧 / 𝑦]∅ ∈ 𝑦 ↔ ∅ ∈ 𝑧)
7	5, 6	sylib 122	. . . 4 ⊢ ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∅ ∈ 𝑧)
8	3, 7	sylbi 121	. . 3 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → ∅ ∈ 𝑧)
9	2, 8	mpgbir 1464	. 2 ⊢ ∅ ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}
10		dfom3 4624	. 2 ⊢ ω = ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}
11	9, 10	eleqtrri 2269	1 ⊢ ∅ ∈ ω

Syntax hints:   → wi 4   ∧ wa 104  [wsb 1773   ∈ wcel 2164  {cab 2179  ∀wral 2472  ∅c0 3446  ∩ cint 3870  suc csuc 4396  ωcom 4622

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-nul 4155

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-dif 3155  df-nul 3447  df-int 3871  df-iom 4623

This theorem is referenced by:  peano5  4630  limom  4646  nnregexmid  4653  omsinds  4654  nnpredcl  4655  frec0g  6450  frecabcl  6452  frecrdg  6461  oa1suc  6520  nna0r  6531  nnm0r  6532  nnmcl  6534  nnmsucr  6541  1onn  6573  nnm1  6578  nnaordex  6581  nnawordex  6582  php5  6914  php5dom  6919  0fin  6940  findcard2  6945  findcard2s  6946  infm  6960  inffiexmid  6962  0ct  7166  ctmlemr  7167  ctssdclemn0  7169  ctssdc  7172  omct  7176  nninfisol  7192  fodjum  7205  fodju0  7206  ctssexmid  7209  nninfwlpoimlemg  7234  nninfwlpoimlemginf  7235  1lt2pi  7400  nq0m0r  7516  nq0a0  7517  prarloclem5  7560  frec2uzrand  10476  frecuzrdg0  10484  frecuzrdg0t  10493  frecfzennn  10497  0tonninf  10511  1tonninf  10512  hashinfom  10849  hashunlem  10875  hash1  10882  nninfctlemfo  12177  ennnfonelemj0  12558  ennnfonelem1  12564  ennnfonelemhf1o  12570  ennnfonelemhom  12572  fnpr2o  12922  fvpr0o  12924  xpscf  12930  bj-nn0suc  15456  bj-nn0sucALT  15470  012of  15486  2o01f  15487  pwle2  15489  pwf1oexmid  15490  subctctexmid  15491  peano3nninf  15497  nninfall  15499  nninfsellemdc  15500  nninfsellemeq  15504  nninffeq  15510  isomninnlem  15520  iswomninnlem  15539  ismkvnnlem  15542