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 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 ) )