Theorem peano1 4685

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 4210	. . . 4 ⊢ ∅ ∈ V
2	1	elint 3928	. . 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 4683	. 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 3922  suc csuc 4455  ωcom 4681

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 4209

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 3923  df-iom 4682

This theorem is referenced by:  peano5  4689  limom  4705  nnregexmid  4712  omsinds  4713  nnpredcl  4714  frec0g  6541  frecabcl  6543  frecrdg  6552  oa1suc  6611  nna0r  6622  nnm0r  6623  nnmcl  6625  nnmsucr  6632  1onn  6664  nnm1  6669  nnaordex  6672  nnawordex  6673  php5  7015  php5dom  7020  0fin  7042  findcard2  7047  findcard2s  7048  infm  7062  inffiexmid  7064  0ct  7270  ctmlemr  7271  ctssdclemn0  7273  ctssdc  7276  omct  7280  nninfisol  7296  fodjum  7309  fodju0  7310  ctssexmid  7313  nninfwlpoimlemg  7338  nninfwlpoimlemginf  7339  1lt2pi  7523  nq0m0r  7639  nq0a0  7640  prarloclem5  7683  frec2uzrand  10622  frecuzrdg0  10630  frecuzrdg0t  10639  frecfzennn  10643  0tonninf  10657  1tonninf  10658  hashinfom  10995  hashunlem  11021  hash1  11028  nninfctlemfo  12556  ennnfonelemj0  12967  ennnfonelem1  12973  ennnfonelemhf1o  12979  ennnfonelemhom  12981  fnpr2o  13367  fvpr0o  13369  xpscf  13375  bj-nn0suc  16285  bj-nn0sucALT  16299  012of  16316  2o01f  16317  pwle2  16323  pwf1oexmid  16324  subctctexmid  16325  peano3nninf  16332  nninfall  16334  nninfsellemdc  16335  nninfsellemeq  16339  nninffeq  16345  nnnninfex  16347  isomninnlem  16357  iswomninnlem  16376  ismkvnnlem  16379