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 \in V \land Fun F) \to \|F\| = \|dom F\|$

Step	Hyp	Ref	Expression
1		hashfun	$⊢ F \in Fin \to (Fun F \leftrightarrow \|F\| = \|dom F\|)$
2	1	biimpd	$⊢ F \in Fin \to (Fun F \to \|F\| = \|dom F\|)$
3	2	adantld	$⊢ F \in Fin \to ((F \in V \land Fun F) \to \|F\| = \|dom F\|)$
4		hashinf	$⊢ (F \in V \land \neg F \in Fin) \to \|F\| = +∞$
5	4	3adant2	$⊢ (F \in V \land Fun F \land \neg F \in Fin) \to \|F\| = +∞$
6		fundmfibi	$⊢ Fun F \to (F \in Fin \leftrightarrow dom F \in Fin)$
7	6	notbid	$⊢ Fun F \to (\neg F \in Fin \leftrightarrow \neg dom F \in Fin)$
8	7	adantl	$⊢ (F \in V \land Fun F) \to (\neg F \in Fin \leftrightarrow \neg dom F \in Fin)$
9		dmexg	$⊢ F \in V \to dom F \in V$
10		hashinf	$⊢ (dom F \in V \land \neg dom F \in Fin) \to \|dom F\| = +∞$
11	9 10	sylan	$⊢ (F \in V \land \neg dom F \in Fin) \to \|dom F\| = +∞$
12	11	ex	$⊢ F \in V \to (\neg dom F \in Fin \to \|dom F\| = +∞)$
13	12	adantr	$⊢ (F \in V \land Fun F) \to (\neg dom F \in Fin \to \|dom F\| = +∞)$
14	8 13	sylbid	$⊢ (F \in V \land Fun F) \to (\neg F \in Fin \to \|dom F\| = +∞)$
15	14	3impia	$⊢ (F \in V \land Fun F \land \neg F \in Fin) \to \|dom F\| = +∞$
16	5 15	eqtr4d	$⊢ (F \in V \land Fun F \land \neg F \in Fin) \to \|F\| = \|dom F\|$
17	16	3comr	$⊢ (\neg F \in Fin \land F \in V \land Fun F) \to \|F\| = \|dom F\|$
18	17	3expib	$⊢ \neg F \in Fin \to ((F \in V \land Fun F) \to \|F\| = \|dom F\|)$
19	3 18	pm2.61i	$⊢ (F \in V \land Fun F) \to \|F\| = \|dom F\|$

Metamath Proof Explorer