hashfn

Description: A function is equinumerous to its domain. (Contributed by Mario Carneiro, 12-Mar-2015)

		Ref	Expression
	Assertion	hashfn	$⊢ F Fn A \to \|F\| = \|A\|$

Step	Hyp	Ref	Expression
1		fndmeng	$⊢ (F Fn A \land A \in V) \to A \approx F$
2		ensym	$⊢ A \approx F \to F \approx A$
3		hasheni	$⊢ F \approx A \to \|F\| = \|A\|$
4	1 2 3	3syl	$⊢ (F Fn A \land A \in V) \to \|F\| = \|A\|$
5		dmexg	$⊢ F \in V \to dom F \in V$
6		fndm	$⊢ F Fn A \to dom F = A$
7	6	eleq1d	$⊢ F Fn A \to (dom F \in V \leftrightarrow A \in V)$
8	5 7	imbitrid	$⊢ F Fn A \to (F \in V \to A \in V)$
9	8	con3dimp	$⊢ (F Fn A \land \neg A \in V) \to \neg F \in V$
10		fvprc	$⊢ \neg F \in V \to \|F\| = \emptyset$
11	9 10	syl	$⊢ (F Fn A \land \neg A \in V) \to \|F\| = \emptyset$
12		fvprc	$⊢ \neg A \in V \to \|A\| = \emptyset$
13	12	adantl	$⊢ (F Fn A \land \neg A \in V) \to \|A\| = \emptyset$
14	11 13	eqtr4d	$⊢ (F Fn A \land \neg A \in V) \to \|F\| = \|A\|$
15	4 14	pm2.61dan	$⊢ F Fn A \to \|F\| = \|A\|$

Metamath Proof Explorer