Metamath Proof Explorer

Theorem hashres

Description: The number of elements of a finite function restricted to a subset of its domain is equal to the number of elements of that subset. (Contributed by AV, 15-Dec-2021)

Ref Expression
Assertion hashres ⊢ Fun ⁡ A ∧ A ∈ Fin ∧ B ⊆ dom ⁡ A → A ↾ B = B

Proof

Step Hyp Ref Expression
1 funres ⊢ Fun ⁡ A → Fun ⁡ A ↾ B
2 1 3ad2ant1 ⊢ Fun ⁡ A ∧ A ∈ Fin ∧ B ⊆ dom ⁡ A → Fun ⁡ A ↾ B
3 finresfin ⊢ A ∈ Fin → A ↾ B ∈ Fin
4 3 3ad2ant2 ⊢ Fun ⁡ A ∧ A ∈ Fin ∧ B ⊆ dom ⁡ A → A ↾ B ∈ Fin
5 hashfun ⊢ A ↾ B ∈ Fin → Fun ⁡ A ↾ B ↔ A ↾ B = dom ⁡ A ↾ B
6 4 5 syl ⊢ Fun ⁡ A ∧ A ∈ Fin ∧ B ⊆ dom ⁡ A → Fun ⁡ A ↾ B ↔ A ↾ B = dom ⁡ A ↾ B
7 2 6 mpbid ⊢ Fun ⁡ A ∧ A ∈ Fin ∧ B ⊆ dom ⁡ A → A ↾ B = dom ⁡ A ↾ B
8 ssdmres ⊢ B ⊆ dom ⁡ A ↔ dom ⁡ A ↾ B = B
9 8 biimpi ⊢ B ⊆ dom ⁡ A → dom ⁡ A ↾ B = B
10 9 3ad2ant3 ⊢ Fun ⁡ A ∧ A ∈ Fin ∧ B ⊆ dom ⁡ A → dom ⁡ A ↾ B = B
11 10 fveq2d ⊢ Fun ⁡ A ∧ A ∈ Fin ∧ B ⊆ dom ⁡ A → dom ⁡ A ↾ B = B
12 7 11 eqtrd ⊢ Fun ⁡ A ∧ A ∈ Fin ∧ B ⊆ dom ⁡ A → A ↾ B = B