Theorem f1rnen

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

	Ref	Expression
Assertion	f1rnen	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ran 𝐹 ≈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		f1fn	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 Fn 𝐴 )
2	1	adantr	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → 𝐹 Fn 𝐴 )
3		fnima	⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 “ 𝐴 ) = ran 𝐹 )
4	2 3	syl	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 “ 𝐴 ) = ran 𝐹 )
5		ssid	⊢ 𝐴 ⊆ 𝐴
6		f1imaeng	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 “ 𝐴 ) ≈ 𝐴 )
7	5 6	mp3an2	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 “ 𝐴 ) ≈ 𝐴 )
8	4 7	eqbrtrrd	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ran 𝐹 ≈ 𝐴 )