Theorem 1nn

Description: Peano postulate: 1 is a positive integer. (Contributed by NM, 11-Jan-1997) (Revised by Mario Carneiro, 17-Nov-2014)

	Ref	Expression
Assertion	1nn	⊢ 1 ∈ ℕ

Proof

Step	Hyp	Ref	Expression
1		1ex	⊢ 1 ∈ V
2		fr0g	⊢ ( 1 ∈ V → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) ‘ ∅ ) = 1 )
3	1 2	ax-mp	⊢ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) ‘ ∅ ) = 1
4		frfnom	⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) Fn ω
5		peano1	⊢ ∅ ∈ ω
6		fnfvelrn	⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) Fn ω ∧ ∅ ∈ ω ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) ‘ ∅ ) ∈ ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) )
7	4 5 6	mp2an	⊢ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) ‘ ∅ ) ∈ ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω )
8	3 7	eqeltrri	⊢ 1 ∈ ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω )
9		df-nn	⊢ ℕ = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) “ ω )
10		df-ima	⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) “ ω ) = ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω )
11	9 10	eqtri	⊢ ℕ = ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω )
12	8 11	eleqtrri	⊢ 1 ∈ ℕ