f1rnen

Description: Equinumerosity of the range of an injective function. (Contributed by Thierry Arnoux, 7-Jul-2023)

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

Step	Hyp	Ref	Expression
1		f1fn	$⊢ F : A \underset{1-1}{⟶} B \to F Fn A$
2	1	adantr	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V) \to F Fn A$
3		fnima	$⊢ F Fn A \to F [A] = ran F$
4	2 3	syl	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V) \to F [A] = ran F$
5		ssid	$⊢ A \subseteq A$
6		f1imaeng	$⊢ (F : A \underset{1-1}{⟶} B \land A \subseteq A \land A \in V) \to F [A] \approx A$
7	5 6	mp3an2	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V) \to F [A] \approx A$
8	4 7	eqbrtrrd	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V) \to ran F \approx A$

Metamath Proof Explorer