Metamath Proof Explorer


Theorem foco

Description: Composition of onto functions. (Contributed by NM, 22-Mar-2006) (Proof shortened by AV, 29-Sep-2024)

Ref Expression
Assertion foco F:BontoCG:AontoBFG:AontoC

Proof

Step Hyp Ref Expression
1 simpl F:BontoCG:AontoBF:BontoC
2 fofun G:AontoBFunG
3 2 adantl F:BontoCG:AontoBFunG
4 forn G:AontoBranG=B
5 eqimss2 ranG=BBranG
6 4 5 syl G:AontoBBranG
7 6 adantl F:BontoCG:AontoBBranG
8 focofo F:BontoCFunGBranGFG:G-1BontoC
9 1 3 7 8 syl3anc F:BontoCG:AontoBFG:G-1BontoC
10 focnvimacdmdm G:AontoBG-1B=A
11 10 eqcomd G:AontoBA=G-1B
12 11 adantl F:BontoCG:AontoBA=G-1B
13 foeq2 A=G-1BFG:AontoCFG:G-1BontoC
14 12 13 syl F:BontoCG:AontoBFG:AontoCFG:G-1BontoC
15 9 14 mpbird F:BontoCG:AontoBFG:AontoC