Theorem peano1 4516

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 4063	. . . 4 ⊢ ∅ ∈ V
2	1	elint 3785	. . 3 ⊢ (∅ ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → ∅ ∈ 𝑧))
3		df-clab 2127	. . . 4 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ [𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦))
4		simpl 108	. . . . . 6 ⊢ ((∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∅ ∈ 𝑦)
5	4	sbimi 1738	. . . . 5 ⊢ ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → [𝑧 / 𝑦]∅ ∈ 𝑦)
6		clelsb4 2246	. . . . 5 ⊢ ([𝑧 / 𝑦]∅ ∈ 𝑦 ↔ ∅ ∈ 𝑧)
7	5, 6	sylib 121	. . . 4 ⊢ ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∅ ∈ 𝑧)
8	3, 7	sylbi 120	. . 3 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → ∅ ∈ 𝑧)
9	2, 8	mpgbir 1430	. 2 ⊢ ∅ ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}
10		dfom3 4514	. 2 ⊢ ω = ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}
11	9, 10	eleqtrri 2216	1 ⊢ ∅ ∈ ω

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1481  [wsb 1736  {cab 2126  ∀wral 2417  ∅c0 3368  ∩ cint 3779  suc csuc 4295  ωcom 4512

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-nul 4062

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691  df-dif 3078  df-nul 3369  df-int 3780  df-iom 4513

This theorem is referenced by:  peano5  4520  limom  4535  nnregexmid  4542  omsinds  4543  nnpredcl  4544  frec0g  6302  frecabcl  6304  frecrdg  6313  oa1suc  6371  nna0r  6382  nnm0r  6383  nnmcl  6385  nnmsucr  6392  1onn  6424  nnm1  6428  nnaordex  6431  nnawordex  6432  php5  6760  php5dom  6765  0fin  6786  findcard2  6791  findcard2s  6792  infm  6806  inffiexmid  6808  0ct  7000  ctmlemr  7001  ctssdclemn0  7003  ctssdc  7006  omct  7010  fodjum  7026  fodju0  7027  ctssexmid  7032  1lt2pi  7172  nq0m0r  7288  nq0a0  7289  prarloclem5  7332  frec2uzrand  10209  frecuzrdg0  10217  frecuzrdg0t  10226  frecfzennn  10230  0tonninf  10243  1tonninf  10244  hashinfom  10556  hashunlem  10582  hash1  10589  ennnfonelemj0  11950  ennnfonelem1  11956  ennnfonelemhf1o  11962  ennnfonelemhom  11964  bj-nn0suc  13333  bj-nn0sucALT  13347  012of  13363  2o01f  13364  pwle2  13366  pwf1oexmid  13367  subctctexmid  13369  peano3nninf  13376  nninfall  13379  nninfsellemdc  13381  nninfsellemeq  13385  nninffeq  13391  isomninnlem  13400  iswomninnlem  13417  ismkvnnlem  13419