hashf1dmrn

Description: The size of the domain of a one-to-one set function is equal to the size of its range. (Contributed by BTernaryTau, 1-Oct-2023)

		Ref	Expression
	Assertion	hashf1dmrn	$⊢ (F \in V \land F : A \underset{1-1}{⟶} B) \to \|A\| = \|ran F\|$

Step	Hyp	Ref	Expression
1		f1fun	$⊢ F : A \underset{1-1}{⟶} B \to Fun F$
2		hashfundm	$⊢ (F \in V \land Fun F) \to \|F\| = \|dom F\|$
3	1 2	sylan2	$⊢ (F \in V \land F : A \underset{1-1}{⟶} B) \to \|F\| = \|dom F\|$
4		f1dm	$⊢ F : A \underset{1-1}{⟶} B \to dom F = A$
5	4	adantl	$⊢ (F \in V \land F : A \underset{1-1}{⟶} B) \to dom F = A$
6		dmexg	$⊢ F \in V \to dom F \in V$
7	6	adantr	$⊢ (F \in V \land F : A \underset{1-1}{⟶} B) \to dom F \in V$
8	5 7	eqeltrrd	$⊢ (F \in V \land F : A \underset{1-1}{⟶} B) \to A \in V$
9		hashf1rn	$⊢ (A \in V \land F : A \underset{1-1}{⟶} B) \to \|F\| = \|ran F\|$
10	8 9	sylancom	$⊢ (F \in V \land F : A \underset{1-1}{⟶} B) \to \|F\| = \|ran F\|$
11	5	fveq2d	$⊢ (F \in V \land F : A \underset{1-1}{⟶} B) \to \|dom F\| = \|A\|$
12	3 10 11	3eqtr3rd	$⊢ (F \in V \land F : A \underset{1-1}{⟶} B) \to \|A\| = \|ran F\|$

Metamath Proof Explorer