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 𝐴𝐴 ∈ Fin ∧ 𝐵 ⊆ dom 𝐴 ) → ( ♯ ‘ ( 𝐴𝐵 ) ) = ( ♯ ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 funres ( Fun 𝐴 → Fun ( 𝐴𝐵 ) )
2 1 3ad2ant1 ( ( Fun 𝐴𝐴 ∈ Fin ∧ 𝐵 ⊆ dom 𝐴 ) → Fun ( 𝐴𝐵 ) )
3 finresfin ( 𝐴 ∈ Fin → ( 𝐴𝐵 ) ∈ Fin )
4 3 3ad2ant2 ( ( Fun 𝐴𝐴 ∈ Fin ∧ 𝐵 ⊆ dom 𝐴 ) → ( 𝐴𝐵 ) ∈ Fin )
5 hashfun ( ( 𝐴𝐵 ) ∈ Fin → ( Fun ( 𝐴𝐵 ) ↔ ( ♯ ‘ ( 𝐴𝐵 ) ) = ( ♯ ‘ dom ( 𝐴𝐵 ) ) ) )
6 4 5 syl ( ( Fun 𝐴𝐴 ∈ Fin ∧ 𝐵 ⊆ dom 𝐴 ) → ( Fun ( 𝐴𝐵 ) ↔ ( ♯ ‘ ( 𝐴𝐵 ) ) = ( ♯ ‘ dom ( 𝐴𝐵 ) ) ) )
7 2 6 mpbid ( ( Fun 𝐴𝐴 ∈ Fin ∧ 𝐵 ⊆ dom 𝐴 ) → ( ♯ ‘ ( 𝐴𝐵 ) ) = ( ♯ ‘ dom ( 𝐴𝐵 ) ) )
8 ssdmres ( 𝐵 ⊆ dom 𝐴 ↔ dom ( 𝐴𝐵 ) = 𝐵 )
9 8 biimpi ( 𝐵 ⊆ dom 𝐴 → dom ( 𝐴𝐵 ) = 𝐵 )
10 9 3ad2ant3 ( ( Fun 𝐴𝐴 ∈ Fin ∧ 𝐵 ⊆ dom 𝐴 ) → dom ( 𝐴𝐵 ) = 𝐵 )
11 10 fveq2d ( ( Fun 𝐴𝐴 ∈ Fin ∧ 𝐵 ⊆ dom 𝐴 ) → ( ♯ ‘ dom ( 𝐴𝐵 ) ) = ( ♯ ‘ 𝐵 ) )
12 7 11 eqtrd ( ( Fun 𝐴𝐴 ∈ Fin ∧ 𝐵 ⊆ dom 𝐴 ) → ( ♯ ‘ ( 𝐴𝐵 ) ) = ( ♯ ‘ 𝐵 ) )