Theorem peano1 4650

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 4179	. . . 4 ⊢ ∅ ∈ V
2	1	elint 3897	. . 3 ⊢ (∅ ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → ∅ ∈ 𝑧))
3		df-clab 2193	. . . 4 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ [𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦))
4		simpl 109	. . . . . 6 ⊢ ((∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∅ ∈ 𝑦)
5	4	sbimi 1788	. . . . 5 ⊢ ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → [𝑧 / 𝑦]∅ ∈ 𝑦)
6		clelsb2 2312	. . . . 5 ⊢ ([𝑧 / 𝑦]∅ ∈ 𝑦 ↔ ∅ ∈ 𝑧)
7	5, 6	sylib 122	. . . 4 ⊢ ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∅ ∈ 𝑧)
8	3, 7	sylbi 121	. . 3 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → ∅ ∈ 𝑧)
9	2, 8	mpgbir 1477	. 2 ⊢ ∅ ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}
10		dfom3 4648	. 2 ⊢ ω = ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}
11	9, 10	eleqtrri 2282	1 ⊢ ∅ ∈ ω

Syntax hints:   → wi 4   ∧ wa 104  [wsb 1786   ∈ wcel 2177  {cab 2192  ∀wral 2485  ∅c0 3464  ∩ cint 3891  suc csuc 4420  ωcom 4646

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188  ax-nul 4178

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-dif 3172  df-nul 3465  df-int 3892  df-iom 4647

This theorem is referenced by:  peano5  4654  limom  4670  nnregexmid  4677  omsinds  4678  nnpredcl  4679  frec0g  6496  frecabcl  6498  frecrdg  6507  oa1suc  6566  nna0r  6577  nnm0r  6578  nnmcl  6580  nnmsucr  6587  1onn  6619  nnm1  6624  nnaordex  6627  nnawordex  6628  php5  6970  php5dom  6975  0fin  6996  findcard2  7001  findcard2s  7002  infm  7016  inffiexmid  7018  0ct  7224  ctmlemr  7225  ctssdclemn0  7227  ctssdc  7230  omct  7234  nninfisol  7250  fodjum  7263  fodju0  7264  ctssexmid  7267  nninfwlpoimlemg  7292  nninfwlpoimlemginf  7293  1lt2pi  7473  nq0m0r  7589  nq0a0  7590  prarloclem5  7633  frec2uzrand  10572  frecuzrdg0  10580  frecuzrdg0t  10589  frecfzennn  10593  0tonninf  10607  1tonninf  10608  hashinfom  10945  hashunlem  10971  hash1  10978  nninfctlemfo  12436  ennnfonelemj0  12847  ennnfonelem1  12853  ennnfonelemhf1o  12859  ennnfonelemhom  12861  fnpr2o  13246  fvpr0o  13248  xpscf  13254  bj-nn0suc  16038  bj-nn0sucALT  16052  012of  16069  2o01f  16070  pwle2  16076  pwf1oexmid  16077  subctctexmid  16078  peano3nninf  16085  nninfall  16087  nninfsellemdc  16088  nninfsellemeq  16092  nninffeq  16098  nnnninfex  16100  isomninnlem  16110  iswomninnlem  16129  ismkvnnlem  16132