Metamath Proof Explorer

Theorem f1oco

Description: Composition of one-to-one onto functions. (Contributed by NM, 19-Mar-1998)

Ref Expression
Assertion f1oco ${⊢}\left({F}:{B}\underset{1-1 onto}{⟶}{C}\wedge {G}:{A}\underset{1-1 onto}{⟶}{B}\right)\to \left({F}\circ {G}\right):{A}\underset{1-1 onto}{⟶}{C}$

Proof

Step Hyp Ref Expression
1 df-f1o ${⊢}{F}:{B}\underset{1-1 onto}{⟶}{C}↔\left({F}:{B}\underset{1-1}{⟶}{C}\wedge {F}:{B}\underset{onto}{⟶}{C}\right)$
2 df-f1o ${⊢}{G}:{A}\underset{1-1 onto}{⟶}{B}↔\left({G}:{A}\underset{1-1}{⟶}{B}\wedge {G}:{A}\underset{onto}{⟶}{B}\right)$
3 f1co ${⊢}\left({F}:{B}\underset{1-1}{⟶}{C}\wedge {G}:{A}\underset{1-1}{⟶}{B}\right)\to \left({F}\circ {G}\right):{A}\underset{1-1}{⟶}{C}$
4 foco ${⊢}\left({F}:{B}\underset{onto}{⟶}{C}\wedge {G}:{A}\underset{onto}{⟶}{B}\right)\to \left({F}\circ {G}\right):{A}\underset{onto}{⟶}{C}$
5 3 4 anim12i ${⊢}\left(\left({F}:{B}\underset{1-1}{⟶}{C}\wedge {G}:{A}\underset{1-1}{⟶}{B}\right)\wedge \left({F}:{B}\underset{onto}{⟶}{C}\wedge {G}:{A}\underset{onto}{⟶}{B}\right)\right)\to \left(\left({F}\circ {G}\right):{A}\underset{1-1}{⟶}{C}\wedge \left({F}\circ {G}\right):{A}\underset{onto}{⟶}{C}\right)$
6 5 an4s ${⊢}\left(\left({F}:{B}\underset{1-1}{⟶}{C}\wedge {F}:{B}\underset{onto}{⟶}{C}\right)\wedge \left({G}:{A}\underset{1-1}{⟶}{B}\wedge {G}:{A}\underset{onto}{⟶}{B}\right)\right)\to \left(\left({F}\circ {G}\right):{A}\underset{1-1}{⟶}{C}\wedge \left({F}\circ {G}\right):{A}\underset{onto}{⟶}{C}\right)$
7 1 2 6 syl2anb ${⊢}\left({F}:{B}\underset{1-1 onto}{⟶}{C}\wedge {G}:{A}\underset{1-1 onto}{⟶}{B}\right)\to \left(\left({F}\circ {G}\right):{A}\underset{1-1}{⟶}{C}\wedge \left({F}\circ {G}\right):{A}\underset{onto}{⟶}{C}\right)$
8 df-f1o ${⊢}\left({F}\circ {G}\right):{A}\underset{1-1 onto}{⟶}{C}↔\left(\left({F}\circ {G}\right):{A}\underset{1-1}{⟶}{C}\wedge \left({F}\circ {G}\right):{A}\underset{onto}{⟶}{C}\right)$
9 7 8 sylibr ${⊢}\left({F}:{B}\underset{1-1 onto}{⟶}{C}\wedge {G}:{A}\underset{1-1 onto}{⟶}{B}\right)\to \left({F}\circ {G}\right):{A}\underset{1-1 onto}{⟶}{C}$