Metamath Proof Explorer

Theorem f1ocnv

Description: The converse of a one-to-one onto function is also one-to-one onto. (Contributed by NM, 11-Feb-1997) (Proof shortened by Andrew Salmon, 22-Oct-2011)

Ref Expression
Assertion f1ocnv ⊢ F : A ⟶ 1-1 onto B → F -1 : B ⟶ 1-1 onto A

Proof

Step Hyp Ref Expression
1 fnrel ⊢ F Fn A → Rel ⁡ F
2 dfrel2 ⊢ Rel ⁡ F ↔ F -1 -1 = F
3 fneq1 ⊢ F -1 -1 = F → F -1 -1 Fn A ↔ F Fn A
4 3 biimprd ⊢ F -1 -1 = F → F Fn A → F -1 -1 Fn A
5 2 4 sylbi ⊢ Rel ⁡ F → F Fn A → F -1 -1 Fn A
6 1 5 mpcom ⊢ F Fn A → F -1 -1 Fn A
7 6 anim1ci ⊢ F Fn A ∧ F -1 Fn B → F -1 Fn B ∧ F -1 -1 Fn A
8 dff1o4 ⊢ F : A ⟶ 1-1 onto B ↔ F Fn A ∧ F -1 Fn B
9 dff1o4 ⊢ F -1 : B ⟶ 1-1 onto A ↔ F -1 Fn B ∧ F -1 -1 Fn A
10 7 8 9 3imtr4i ⊢ F : A ⟶ 1-1 onto B → F -1 : B ⟶ 1-1 onto A