# Metamath Proof Explorer

## Theorem fcof1o

Description: Show that two functions are inverse to each other by computing their compositions. (Contributed by Mario Carneiro, 21-Mar-2015) (Proof shortened by AV, 15-Dec-2019)

Ref Expression
Assertion fcof1o ${⊢}\left(\left({F}:{A}⟶{B}\wedge {G}:{B}⟶{A}\right)\wedge \left({F}\circ {G}={\mathrm{I}↾}_{{B}}\wedge {G}\circ {F}={\mathrm{I}↾}_{{A}}\right)\right)\to \left({F}:{A}\underset{1-1 onto}{⟶}{B}\wedge {{F}}^{-1}={G}\right)$

### Proof

Step Hyp Ref Expression
1 simpll ${⊢}\left(\left({F}:{A}⟶{B}\wedge {G}:{B}⟶{A}\right)\wedge \left({F}\circ {G}={\mathrm{I}↾}_{{B}}\wedge {G}\circ {F}={\mathrm{I}↾}_{{A}}\right)\right)\to {F}:{A}⟶{B}$
2 simplr ${⊢}\left(\left({F}:{A}⟶{B}\wedge {G}:{B}⟶{A}\right)\wedge \left({F}\circ {G}={\mathrm{I}↾}_{{B}}\wedge {G}\circ {F}={\mathrm{I}↾}_{{A}}\right)\right)\to {G}:{B}⟶{A}$
3 simprr ${⊢}\left(\left({F}:{A}⟶{B}\wedge {G}:{B}⟶{A}\right)\wedge \left({F}\circ {G}={\mathrm{I}↾}_{{B}}\wedge {G}\circ {F}={\mathrm{I}↾}_{{A}}\right)\right)\to {G}\circ {F}={\mathrm{I}↾}_{{A}}$
4 simprl ${⊢}\left(\left({F}:{A}⟶{B}\wedge {G}:{B}⟶{A}\right)\wedge \left({F}\circ {G}={\mathrm{I}↾}_{{B}}\wedge {G}\circ {F}={\mathrm{I}↾}_{{A}}\right)\right)\to {F}\circ {G}={\mathrm{I}↾}_{{B}}$
5 1 2 3 4 fcof1od ${⊢}\left(\left({F}:{A}⟶{B}\wedge {G}:{B}⟶{A}\right)\wedge \left({F}\circ {G}={\mathrm{I}↾}_{{B}}\wedge {G}\circ {F}={\mathrm{I}↾}_{{A}}\right)\right)\to {F}:{A}\underset{1-1 onto}{⟶}{B}$
6 1 2 3 4 2fcoidinvd ${⊢}\left(\left({F}:{A}⟶{B}\wedge {G}:{B}⟶{A}\right)\wedge \left({F}\circ {G}={\mathrm{I}↾}_{{B}}\wedge {G}\circ {F}={\mathrm{I}↾}_{{A}}\right)\right)\to {{F}}^{-1}={G}$
7 5 6 jca ${⊢}\left(\left({F}:{A}⟶{B}\wedge {G}:{B}⟶{A}\right)\wedge \left({F}\circ {G}={\mathrm{I}↾}_{{B}}\wedge {G}\circ {F}={\mathrm{I}↾}_{{A}}\right)\right)\to \left({F}:{A}\underset{1-1 onto}{⟶}{B}\wedge {{F}}^{-1}={G}\right)$