Theorem hashcl

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

	Ref	Expression
Assertion	hashcl	⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω )
2	1	hashgval	⊢ ( 𝐴 ∈ Fin → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐴 ) ) = ( ♯ ‘ 𝐴 ) )
3		ficardom	⊢ ( 𝐴 ∈ Fin → ( card ‘ 𝐴 ) ∈ ω )
4	1	hashgf1o	⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) : ω –1-1-onto→ ℕ0
5		f1of	⊢ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) : ω –1-1-onto→ ℕ0 → ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) : ω ⟶ ℕ0 )
6	4 5	ax-mp	⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) : ω ⟶ ℕ0
7	6	ffvelrni	⊢ ( ( card ‘ 𝐴 ) ∈ ω → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐴 ) ) ∈ ℕ0 )
8	3 7	syl	⊢ ( 𝐴 ∈ Fin → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐴 ) ) ∈ ℕ0 )
9	2 8	eqeltrrd	⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )