This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐴 ) → ( ♯ ‘ ( 𝐴 ↾ 𝐵 ) ) = ( ♯ ‘ 𝐵 ) )