hashcl

Description: Closure of the # function. (Contributed by Paul Chapman, 26-Oct-2012) (Revised by Mario Carneiro, 13-Jul-2014)

		Ref	Expression
	Assertion	hashcl	$⊢ A \in Fin \to \|A\| \in ℕ_{0}$

Step	Hyp	Ref	Expression
1		eqid	$⊢ {rec ((x \in V ⟼ x + 1), 0) ↾}_{ω} = {rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}$
2	1	hashgval	$⊢ A \in Fin \to ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) (card (A)) = \|A\|$
3		ficardom	$⊢ A \in Fin \to card (A) \in ω$
4	1	hashgf1o	$⊢ ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) : ω \underset{1-1 onto}{⟶} ℕ_{0}$
5		f1of	$⊢ ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) : ω \underset{1-1 onto}{⟶} ℕ_{0} \to ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) : ω ⟶ ℕ_{0}$
6	4 5	ax-mp	$⊢ ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) : ω ⟶ ℕ_{0}$
7	6	ffvelcdmi	$⊢ card (A) \in ω \to ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) (card (A)) \in ℕ_{0}$
8	3 7	syl	$⊢ A \in Fin \to ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) (card (A)) \in ℕ_{0}$
9	2 8	eqeltrrd	$⊢ A \in Fin \to \|A\| \in ℕ_{0}$

Metamath Proof Explorer