Theorem f1rnen

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

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

Proof

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