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 : B -onto-> C /\ G : A -onto-> B ) -> ( F o. G ) : A -onto-> C )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( F : B -onto-> C /\ G : A -onto-> B ) -> F : B -onto-> C )
2 fofun 
 |-  ( G : A -onto-> B -> Fun G )
3 2 adantl 
 |-  ( ( F : B -onto-> C /\ G : A -onto-> B ) -> Fun G )
4 forn 
 |-  ( G : A -onto-> B -> ran G = B )
5 eqimss2 
 |-  ( ran G = B -> B C_ ran G )
6 4 5 syl 
 |-  ( G : A -onto-> B -> B C_ ran G )
7 6 adantl 
 |-  ( ( F : B -onto-> C /\ G : A -onto-> B ) -> B C_ ran G )
8 focofo 
 |-  ( ( F : B -onto-> C /\ Fun G /\ B C_ ran G ) -> ( F o. G ) : ( `' G " B ) -onto-> C )
9 1 3 7 8 syl3anc 
 |-  ( ( F : B -onto-> C /\ G : A -onto-> B ) -> ( F o. G ) : ( `' G " B ) -onto-> C )
10 focnvimacdmdm 
 |-  ( G : A -onto-> B -> ( `' G " B ) = A )
11 10 eqcomd 
 |-  ( G : A -onto-> B -> A = ( `' G " B ) )
12 11 adantl 
 |-  ( ( F : B -onto-> C /\ G : A -onto-> B ) -> A = ( `' G " B ) )
13 foeq2 
 |-  ( A = ( `' G " B ) -> ( ( F o. G ) : A -onto-> C <-> ( F o. G ) : ( `' G " B ) -onto-> C ) )
14 12 13 syl 
 |-  ( ( F : B -onto-> C /\ G : A -onto-> B ) -> ( ( F o. G ) : A -onto-> C <-> ( F o. G ) : ( `' G " B ) -onto-> C ) )
15 9 14 mpbird 
 |-  ( ( F : B -onto-> C /\ G : A -onto-> B ) -> ( F o. G ) : A -onto-> C )