Theorem f1f1orn

Description: A one-to-one function maps one-to-one onto its range. (Contributed by NM, 4-Sep-2004)

	Ref	Expression
Assertion	f1f1orn	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		f1fn	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 Fn 𝐴 )
2		df-f1	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Fun ◡ 𝐹 ) )
3	2	simprbi	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → Fun ◡ 𝐹 )
4		f1orn	⊢ ( 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 ↔ ( 𝐹 Fn 𝐴 ∧ Fun ◡ 𝐹 ) )
5	1 3 4	sylanbrc	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 )