Theorem hashfundm

Description: The size of a set function is equal to the size of its domain. (Contributed by BTernaryTau, 30-Sep-2023)

	Ref	Expression
Assertion	hashfundm	|- ( ( F e. V /\ Fun F ) -> ( # ` F ) = ( # ` dom F ) )

Proof

Step	Hyp	Ref	Expression
1		hashfun	|- ( F e. Fin -> ( Fun F <-> ( # ` F ) = ( # ` dom F ) ) )
2	1	biimpd	|- ( F e. Fin -> ( Fun F -> ( # ` F ) = ( # ` dom F ) ) )
3	2	adantld	|- ( F e. Fin -> ( ( F e. V /\ Fun F ) -> ( # ` F ) = ( # ` dom F ) ) )
4		hashinf	|- ( ( F e. V /\ -. F e. Fin ) -> ( # ` F ) = +oo )
5	4	3adant2	|- ( ( F e. V /\ Fun F /\ -. F e. Fin ) -> ( # ` F ) = +oo )
6		fundmfibi	|- ( Fun F -> ( F e. Fin <-> dom F e. Fin ) )
7	6	notbid	|- ( Fun F -> ( -. F e. Fin <-> -. dom F e. Fin ) )
8	7	adantl	|- ( ( F e. V /\ Fun F ) -> ( -. F e. Fin <-> -. dom F e. Fin ) )
9		dmexg	|- ( F e. V -> dom F e. _V )
10		hashinf	|- ( ( dom F e. _V /\ -. dom F e. Fin ) -> ( # ` dom F ) = +oo )
11	9 10	sylan	|- ( ( F e. V /\ -. dom F e. Fin ) -> ( # ` dom F ) = +oo )
12	11	ex	|- ( F e. V -> ( -. dom F e. Fin -> ( # ` dom F ) = +oo ) )
13	12	adantr	|- ( ( F e. V /\ Fun F ) -> ( -. dom F e. Fin -> ( # ` dom F ) = +oo ) )
14	8 13	sylbid	|- ( ( F e. V /\ Fun F ) -> ( -. F e. Fin -> ( # ` dom F ) = +oo ) )
15	14	3impia	|- ( ( F e. V /\ Fun F /\ -. F e. Fin ) -> ( # ` dom F ) = +oo )
16	5 15	eqtr4d	|- ( ( F e. V /\ Fun F /\ -. F e. Fin ) -> ( # ` F ) = ( # ` dom F ) )
17	16	3comr	|- ( ( -. F e. Fin /\ F e. V /\ Fun F ) -> ( # ` F ) = ( # ` dom F ) )
18	17	3expib	|- ( -. F e. Fin -> ( ( F e. V /\ Fun F ) -> ( # ` F ) = ( # ` dom F ) ) )
19	3 18	pm2.61i	|- ( ( F e. V /\ Fun F ) -> ( # ` F ) = ( # ` dom F ) )