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 \in ℕ$

Step	Hyp	Ref	Expression
1		1ex	$⊢ 1 \in V$
2		fr0g	$⊢ 1 \in V \to ({rec ((x \in V ⟼ x + 1), 1) ↾}_{ω}) (\emptyset) = 1$
3	1 2	ax-mp	$⊢ ({rec ((x \in V ⟼ x + 1), 1) ↾}_{ω}) (\emptyset) = 1$
4		frfnom	$⊢ ({rec ((x \in V ⟼ x + 1), 1) ↾}_{ω}) Fn ω$
5		peano1	$⊢ \emptyset \in ω$
6		fnfvelrn	$⊢ (({rec ((x \in V ⟼ x + 1), 1) ↾}_{ω}) Fn ω \land \emptyset \in ω) \to ({rec ((x \in V ⟼ x + 1), 1) ↾}_{ω}) (\emptyset) \in ran ({rec ((x \in V ⟼ x + 1), 1) ↾}_{ω})$
7	4 5 6	mp2an	$⊢ ({rec ((x \in V ⟼ x + 1), 1) ↾}_{ω}) (\emptyset) \in ran ({rec ((x \in V ⟼ x + 1), 1) ↾}_{ω})$
8	3 7	eqeltrri	$⊢ 1 \in ran ({rec ((x \in V ⟼ x + 1), 1) ↾}_{ω})$
9		df-nn	$⊢ ℕ = rec ((x \in V ⟼ x + 1), 1) [ω]$
10		df-ima	$⊢ rec ((x \in V ⟼ x + 1), 1) [ω] = ran ({rec ((x \in V ⟼ x + 1), 1) ↾}_{ω})$
11	9 10	eqtri	$⊢ ℕ = ran ({rec ((x \in V ⟼ x + 1), 1) ↾}_{ω})$
12	8 11	eleqtrri	$⊢ 1 \in ℕ$

Metamath Proof Explorer