# 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}\underset{1-1 onto}{⟶}{B}\to {{F}}^{-1}:{B}\underset{1-1 onto}{⟶}{A}$

### Proof

Step Hyp Ref Expression
1 fnrel ${⊢}{F}Fn{A}\to \mathrm{Rel}{F}$
2 dfrel2 ${⊢}\mathrm{Rel}{F}↔{{{F}}^{-1}}^{-1}={F}$
3 fneq1 ${⊢}{{{F}}^{-1}}^{-1}={F}\to \left({{{F}}^{-1}}^{-1}Fn{A}↔{F}Fn{A}\right)$
4 3 biimprd ${⊢}{{{F}}^{-1}}^{-1}={F}\to \left({F}Fn{A}\to {{{F}}^{-1}}^{-1}Fn{A}\right)$
5 2 4 sylbi ${⊢}\mathrm{Rel}{F}\to \left({F}Fn{A}\to {{{F}}^{-1}}^{-1}Fn{A}\right)$
6 1 5 mpcom ${⊢}{F}Fn{A}\to {{{F}}^{-1}}^{-1}Fn{A}$
7 6 anim1ci ${⊢}\left({F}Fn{A}\wedge {{F}}^{-1}Fn{B}\right)\to \left({{F}}^{-1}Fn{B}\wedge {{{F}}^{-1}}^{-1}Fn{A}\right)$
8 dff1o4 ${⊢}{F}:{A}\underset{1-1 onto}{⟶}{B}↔\left({F}Fn{A}\wedge {{F}}^{-1}Fn{B}\right)$
9 dff1o4 ${⊢}{{F}}^{-1}:{B}\underset{1-1 onto}{⟶}{A}↔\left({{F}}^{-1}Fn{B}\wedge {{{F}}^{-1}}^{-1}Fn{A}\right)$
10 7 8 9 3imtr4i ${⊢}{F}:{A}\underset{1-1 onto}{⟶}{B}\to {{F}}^{-1}:{B}\underset{1-1 onto}{⟶}{A}$