Theorem peano1 4641

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 4170	. . . 4 ⊢ ∅ ∈ V
2	1	elint 3890	. . 3 ⊢ (∅ ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → ∅ ∈ 𝑧))
3		df-clab 2191	. . . 4 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ [𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦))
4		simpl 109	. . . . . 6 ⊢ ((∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∅ ∈ 𝑦)
5	4	sbimi 1786	. . . . 5 ⊢ ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → [𝑧 / 𝑦]∅ ∈ 𝑦)
6		clelsb2 2310	. . . . 5 ⊢ ([𝑧 / 𝑦]∅ ∈ 𝑦 ↔ ∅ ∈ 𝑧)
7	5, 6	sylib 122	. . . 4 ⊢ ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∅ ∈ 𝑧)
8	3, 7	sylbi 121	. . 3 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → ∅ ∈ 𝑧)
9	2, 8	mpgbir 1475	. 2 ⊢ ∅ ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}
10		dfom3 4639	. 2 ⊢ ω = ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}
11	9, 10	eleqtrri 2280	1 ⊢ ∅ ∈ ω

Syntax hints:   → wi 4   ∧ wa 104  [wsb 1784   ∈ wcel 2175  {cab 2190  ∀wral 2483  ∅c0 3459  ∩ cint 3884  suc csuc 4411  ωcom 4637

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186  ax-nul 4169

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-dif 3167  df-nul 3460  df-int 3885  df-iom 4638

This theorem is referenced by:  peano5  4645  limom  4661  nnregexmid  4668  omsinds  4669  nnpredcl  4670  frec0g  6482  frecabcl  6484  frecrdg  6493  oa1suc  6552  nna0r  6563  nnm0r  6564  nnmcl  6566  nnmsucr  6573  1onn  6605  nnm1  6610  nnaordex  6613  nnawordex  6614  php5  6954  php5dom  6959  0fin  6980  findcard2  6985  findcard2s  6986  infm  7000  inffiexmid  7002  0ct  7208  ctmlemr  7209  ctssdclemn0  7211  ctssdc  7214  omct  7218  nninfisol  7234  fodjum  7247  fodju0  7248  ctssexmid  7251  nninfwlpoimlemg  7276  nninfwlpoimlemginf  7277  1lt2pi  7452  nq0m0r  7568  nq0a0  7569  prarloclem5  7612  frec2uzrand  10548  frecuzrdg0  10556  frecuzrdg0t  10565  frecfzennn  10569  0tonninf  10583  1tonninf  10584  hashinfom  10921  hashunlem  10947  hash1  10954  nninfctlemfo  12303  ennnfonelemj0  12714  ennnfonelem1  12720  ennnfonelemhf1o  12726  ennnfonelemhom  12728  fnpr2o  13113  fvpr0o  13115  xpscf  13121  bj-nn0suc  15833  bj-nn0sucALT  15847  012of  15863  2o01f  15864  pwle2  15868  pwf1oexmid  15869  subctctexmid  15870  peano3nninf  15877  nninfall  15879  nninfsellemdc  15880  nninfsellemeq  15884  nninffeq  15890  nnnninfex  15892  isomninnlem  15902  iswomninnlem  15921  ismkvnnlem  15924