Metamath Proof Explorer

Theorem hashf1dmcdm

Description: The size of the domain of a one-to-one set function is less than or equal to the size of its codomain, if it exists. (Contributed by BTernaryTau, 1-Oct-2023)

		Ref	Expression
	Assertion	hashf1dmcdm	$⊢ (F \in V \land B \in W \land F : A \underset{1-1}{⟶} B) \to \|A\| \leq \|B\|$

Proof

Step	Hyp	Ref	Expression
1		hashf1dmrn	$⊢ (F \in V \land F : A \underset{1-1}{⟶} B) \to \|A\| = \|ran F\|$
2	1	3adant2	$⊢ (F \in V \land B \in W \land F : A \underset{1-1}{⟶} B) \to \|A\| = \|ran F\|$
3		f1f	$⊢ F : A \underset{1-1}{⟶} B \to F : A ⟶ B$
4		frn	$⊢ F : A ⟶ B \to ran F \subseteq B$
5		hashss	$⊢ (B \in W \land ran F \subseteq B) \to \|ran F\| \leq \|B\|$
6	4 5	sylan2	$⊢ (B \in W \land F : A ⟶ B) \to \|ran F\| \leq \|B\|$
7	3 6	sylan2	$⊢ (B \in W \land F : A \underset{1-1}{⟶} B) \to \|ran F\| \leq \|B\|$
8	7	3adant1	$⊢ (F \in V \land B \in W \land F : A \underset{1-1}{⟶} B) \to \|ran F\| \leq \|B\|$
9	2 8	eqbrtrd	$⊢ (F \in V \land B \in W \land F : A \underset{1-1}{⟶} B) \to \|A\| \leq \|B\|$