# Metamath Proof Explorer

## Theorem fcof1od

Description: A function is bijective if a "retraction" and a "section" exist, see comments for fcof1 and fcofo . Formerly part of proof of fcof1o . (Contributed by Mario Carneiro, 21-Mar-2015) (Revised by AV, 15-Dec-2019)

Ref Expression
Hypotheses fcof1od.f ${⊢}{\phi }\to {F}:{A}⟶{B}$
fcof1od.g ${⊢}{\phi }\to {G}:{B}⟶{A}$
fcof1od.a ${⊢}{\phi }\to {G}\circ {F}={\mathrm{I}↾}_{{A}}$
fcof1od.b ${⊢}{\phi }\to {F}\circ {G}={\mathrm{I}↾}_{{B}}$
Assertion fcof1od ${⊢}{\phi }\to {F}:{A}\underset{1-1 onto}{⟶}{B}$

### Proof

Step Hyp Ref Expression
1 fcof1od.f ${⊢}{\phi }\to {F}:{A}⟶{B}$
2 fcof1od.g ${⊢}{\phi }\to {G}:{B}⟶{A}$
3 fcof1od.a ${⊢}{\phi }\to {G}\circ {F}={\mathrm{I}↾}_{{A}}$
4 fcof1od.b ${⊢}{\phi }\to {F}\circ {G}={\mathrm{I}↾}_{{B}}$
5 fcof1 ${⊢}\left({F}:{A}⟶{B}\wedge {G}\circ {F}={\mathrm{I}↾}_{{A}}\right)\to {F}:{A}\underset{1-1}{⟶}{B}$
6 1 3 5 syl2anc ${⊢}{\phi }\to {F}:{A}\underset{1-1}{⟶}{B}$
7 fcofo ${⊢}\left({F}:{A}⟶{B}\wedge {G}:{B}⟶{A}\wedge {F}\circ {G}={\mathrm{I}↾}_{{B}}\right)\to {F}:{A}\underset{onto}{⟶}{B}$
8 1 2 4 7 syl3anc ${⊢}{\phi }\to {F}:{A}\underset{onto}{⟶}{B}$
9 df-f1o ${⊢}{F}:{A}\underset{1-1 onto}{⟶}{B}↔\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {F}:{A}\underset{onto}{⟶}{B}\right)$
10 6 8 9 sylanbrc ${⊢}{\phi }\to {F}:{A}\underset{1-1 onto}{⟶}{B}$