hashfz1

Description: The set ( 1 ... N ) has N elements. (Contributed by Paul Chapman, 22-Jun-2011) (Revised by Mario Carneiro, 15-Sep-2013)

		Ref	Expression
	Assertion	hashfz1	$⊢ N \in ℕ_{0} \to \|(1 \dots N)\| = N$

Step	Hyp	Ref	Expression
1		eqid	$⊢ {rec ((x \in V ⟼ x + 1), 0) ↾}_{ω} = {rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}$
2	1	cardfz	$⊢ N \in ℕ_{0} \to card ((1 \dots N)) = {({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω})}^{-1} (N)$
3	2	fveq2d	$⊢ N \in ℕ_{0} \to ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) (card ((1 \dots N))) = ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) ({({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω})}^{-1} (N))$
4		fzfid	$⊢ N \in ℕ_{0} \to (1 \dots N) \in Fin$
5	1	hashgval	$⊢ (1 \dots N) \in Fin \to ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) (card ((1 \dots N))) = \|(1 \dots N)\|$
6	4 5	syl	$⊢ N \in ℕ_{0} \to ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) (card ((1 \dots N))) = \|(1 \dots N)\|$
7	1	hashgf1o	$⊢ ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) : ω \underset{1-1 onto}{⟶} ℕ_{0}$
8		f1ocnvfv2	$⊢ (({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) : ω \underset{1-1 onto}{⟶} ℕ_{0} \land N \in ℕ_{0}) \to ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) ({({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω})}^{-1} (N)) = N$
9	7 8	mpan	$⊢ N \in ℕ_{0} \to ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) ({({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω})}^{-1} (N)) = N$
10	3 6 9	3eqtr3d	$⊢ N \in ℕ_{0} \to \|(1 \dots N)\| = N$

Metamath Proof Explorer