Metamath Proof Explorer

Theorem f1oco

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

Ref Expression
Assertion f1oco 
|- ( ( F : B -1-1-onto-> C /\ G : A -1-1-onto-> B ) -> ( F o. G ) : A -1-1-onto-> C )

Proof

Step Hyp Ref Expression
1 df-f1o 
 |-  ( F : B -1-1-onto-> C <-> ( F : B -1-1-> C /\ F : B -onto-> C ) )
2 df-f1o 
 |-  ( G : A -1-1-onto-> B <-> ( G : A -1-1-> B /\ G : A -onto-> B ) )
3 f1co 
 |-  ( ( F : B -1-1-> C /\ G : A -1-1-> B ) -> ( F o. G ) : A -1-1-> C )
4 foco 
 |-  ( ( F : B -onto-> C /\ G : A -onto-> B ) -> ( F o. G ) : A -onto-> C )
5 3 4 anim12i 
 |-  ( ( ( F : B -1-1-> C /\ G : A -1-1-> B ) /\ ( F : B -onto-> C /\ G : A -onto-> B ) ) -> ( ( F o. G ) : A -1-1-> C /\ ( F o. G ) : A -onto-> C ) )
6 5 an4s 
 |-  ( ( ( F : B -1-1-> C /\ F : B -onto-> C ) /\ ( G : A -1-1-> B /\ G : A -onto-> B ) ) -> ( ( F o. G ) : A -1-1-> C /\ ( F o. G ) : A -onto-> C ) )
7 1 2 6 syl2anb 
 |-  ( ( F : B -1-1-onto-> C /\ G : A -1-1-onto-> B ) -> ( ( F o. G ) : A -1-1-> C /\ ( F o. G ) : A -onto-> C ) )
8 df-f1o 
 |-  ( ( F o. G ) : A -1-1-onto-> C <-> ( ( F o. G ) : A -1-1-> C /\ ( F o. G ) : A -onto-> C ) )
9 7 8 sylibr 
 |-  ( ( F : B -1-1-onto-> C /\ G : A -1-1-onto-> B ) -> ( F o. G ) : A -1-1-onto-> C )