Theorem peano1 4594

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 4131	. . . 4 ⊢ ∅ ∈ V
2	1	elint 3851	. . 3 ⊢ (∅ ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → ∅ ∈ 𝑧))
3		df-clab 2164	. . . 4 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ [𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦))
4		simpl 109	. . . . . 6 ⊢ ((∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∅ ∈ 𝑦)
5	4	sbimi 1764	. . . . 5 ⊢ ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → [𝑧 / 𝑦]∅ ∈ 𝑦)
6		clelsb2 2283	. . . . 5 ⊢ ([𝑧 / 𝑦]∅ ∈ 𝑦 ↔ ∅ ∈ 𝑧)
7	5, 6	sylib 122	. . . 4 ⊢ ([𝑧 / 𝑦](∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) → ∅ ∈ 𝑧)
8	3, 7	sylbi 121	. . 3 ⊢ (𝑧 ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → ∅ ∈ 𝑧)
9	2, 8	mpgbir 1453	. 2 ⊢ ∅ ∈ ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}
10		dfom3 4592	. 2 ⊢ ω = ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}
11	9, 10	eleqtrri 2253	1 ⊢ ∅ ∈ ω

Syntax hints:   → wi 4   ∧ wa 104  [wsb 1762   ∈ wcel 2148  {cab 2163  ∀wral 2455  ∅c0 3423  ∩ cint 3845  suc csuc 4366  ωcom 4590

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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-nul 4130

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2740  df-dif 3132  df-nul 3424  df-int 3846  df-iom 4591

This theorem is referenced by:  peano5  4598  limom  4614  nnregexmid  4621  omsinds  4622  nnpredcl  4623  frec0g  6398  frecabcl  6400  frecrdg  6409  oa1suc  6468  nna0r  6479  nnm0r  6480  nnmcl  6482  nnmsucr  6489  1onn  6521  nnm1  6526  nnaordex  6529  nnawordex  6530  php5  6858  php5dom  6863  0fin  6884  findcard2  6889  findcard2s  6890  infm  6904  inffiexmid  6906  0ct  7106  ctmlemr  7107  ctssdclemn0  7109  ctssdc  7112  omct  7116  nninfisol  7131  fodjum  7144  fodju0  7145  ctssexmid  7148  nninfwlpoimlemg  7173  nninfwlpoimlemginf  7174  1lt2pi  7339  nq0m0r  7455  nq0a0  7456  prarloclem5  7499  frec2uzrand  10405  frecuzrdg0  10413  frecuzrdg0t  10422  frecfzennn  10426  0tonninf  10439  1tonninf  10440  hashinfom  10758  hashunlem  10784  hash1  10791  ennnfonelemj0  12402  ennnfonelem1  12408  ennnfonelemhf1o  12414  ennnfonelemhom  12416  fnpr2o  12758  fvpr0o  12760  xpscf  12766  bj-nn0suc  14719  bj-nn0sucALT  14733  012of  14748  2o01f  14749  pwle2  14751  pwf1oexmid  14752  subctctexmid  14753  peano3nninf  14759  nninfall  14761  nninfsellemdc  14762  nninfsellemeq  14766  nninffeq  14772  isomninnlem  14781  iswomninnlem  14800  ismkvnnlem  14803