This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem peano1

Description: Zero is a natural number. One of Peano's five postulates for arithmetic. Proposition 7.30(1) of TakeutiZaring p. 42. Note: Unlike most textbooks, our proofs of peano1 through peano5 do not use the Axiom of Infinity. Unlike Takeuti and Zaring, they also do not use the Axiom of Regularity. (Contributed by NM, 15-May-1994) Avoid ax-un . (Revised by BTernaryTau, 29-Nov-2024)

		Ref	Expression
	Assertion	peano1	⊢ ∅ ∈ ω

Proof

Step	Hyp	Ref	Expression
1		0elon	⊢ ∅ ∈ On
2		0ellim	⊢ ( Lim 𝑥 → ∅ ∈ 𝑥 )
3	2	ax-gen	⊢ ∀ 𝑥 ( Lim 𝑥 → ∅ ∈ 𝑥 )
4		elom	⊢ ( ∅ ∈ ω ↔ ( ∅ ∈ On ∧ ∀ 𝑥 ( Lim 𝑥 → ∅ ∈ 𝑥 ) ) )
5	1 3 4	mpbir2an	⊢ ∅ ∈ ω