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