Metamath Proof Explorer

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 ⊢ A ∈ Fin → A ∈ ℕ 0

Proof

Step Hyp Ref Expression
1 eqid ⊢ rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω = rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω
2 1 hashgval ⊢ A ∈ Fin → rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ⁡ card ⁡ A = A
3 ficardom ⊢ A ∈ Fin → card ⁡ A ∈ ω
4 1 hashgf1o ⊢ rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω : ω ⟶ 1-1 onto ℕ 0
5 f1of ⊢ rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω : ω ⟶ 1-1 onto ℕ 0 → rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω : ω ⟶ ℕ 0
6 4 5 ax-mp ⊢ rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω : ω ⟶ ℕ 0
7 6 ffvelcdmi ⊢ card ⁡ A ∈ ω → rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ⁡ card ⁡ A ∈ ℕ 0
8 3 7 syl ⊢ A ∈ Fin → rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ⁡ card ⁡ A ∈ ℕ 0
9 2 8 eqeltrrd ⊢ A ∈ Fin → A ∈ ℕ 0