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