Metamath Proof Explorer

Theorem f1orn

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

Ref Expression
Assertion f1orn ⊢ F : A ⟶ 1-1 onto ran ⁡ F ↔ F Fn A ∧ Fun ⁡ F -1

Proof

Step Hyp Ref Expression
1 dff1o2 ⊢ F : A ⟶ 1-1 onto ran ⁡ F ↔ F Fn A ∧ Fun ⁡ F -1 ∧ ran ⁡ F = ran ⁡ F
2 eqid ⊢ ran ⁡ F = ran ⁡ F
3 df-3an ⊢ F Fn A ∧ Fun ⁡ F -1 ∧ ran ⁡ F = ran ⁡ F ↔ F Fn A ∧ Fun ⁡ F -1 ∧ ran ⁡ F = ran ⁡ F
4 2 3 mpbiran2 ⊢ F Fn A ∧ Fun ⁡ F -1 ∧ ran ⁡ F = ran ⁡ F ↔ F Fn A ∧ Fun ⁡ F -1
5 1 4 bitri ⊢ F : A ⟶ 1-1 onto ran ⁡ F ↔ F Fn A ∧ Fun ⁡ F -1