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 e. Fin /\ B C_ dom A ) -> ( # ` ( A |` B ) ) = ( # ` B ) )

Proof

Step	Hyp	Ref	Expression
1		funres	|- ( Fun A -> Fun ( A |` B ) )
2	1	3ad2ant1	|- ( ( Fun A /\ A e. Fin /\ B C_ dom A ) -> Fun ( A |` B ) )
3		finresfin	|- ( A e. Fin -> ( A |` B ) e. Fin )
4	3	3ad2ant2	|- ( ( Fun A /\ A e. Fin /\ B C_ dom A ) -> ( A |` B ) e. Fin )
5		hashfun	|- ( ( A |` B ) e. Fin -> ( Fun ( A |` B ) <-> ( # ` ( A |` B ) ) = ( # ` dom ( A |` B ) ) ) )
6	4 5	syl	|- ( ( Fun A /\ A e. Fin /\ B C_ dom A ) -> ( Fun ( A |` B ) <-> ( # ` ( A |` B ) ) = ( # ` dom ( A |` B ) ) ) )
7	2 6	mpbid	|- ( ( Fun A /\ A e. Fin /\ B C_ dom A ) -> ( # ` ( A |` B ) ) = ( # ` dom ( A |` B ) ) )
8		ssdmres	|- ( B C_ dom A <-> dom ( A |` B ) = B )
9	8	biimpi	|- ( B C_ dom A -> dom ( A |` B ) = B )
10	9	3ad2ant3	|- ( ( Fun A /\ A e. Fin /\ B C_ dom A ) -> dom ( A |` B ) = B )
11	10	fveq2d	|- ( ( Fun A /\ A e. Fin /\ B C_ dom A ) -> ( # ` dom ( A |` B ) ) = ( # ` B ) )
12	7 11	eqtrd	|- ( ( Fun A /\ A e. Fin /\ B C_ dom A ) -> ( # ` ( A |` B ) ) = ( # ` B ) )