Metamath Proof Explorer

Theorem f1ocof1ob2

Description: If the range of F equals the domain of G , then the composition ( G o. F ) is bijective iff F and G are both bijective. Symmetric version of f1ocof1ob including the fact that F is a surjection onto its range. (Contributed by GL and AV, 20-Sep-2024) (Proof shortened by AV, 7-Oct-2024)

Ref Expression
Assertion f1ocof1ob2 
|- ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> ( ( G o. F ) : A -1-1-onto-> D <-> ( F : A -1-1-onto-> C /\ G : C -1-1-onto-> D ) ) )

Proof

Step Hyp Ref Expression
1 f1ocof1ob 
 |-  ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> ( ( G o. F ) : A -1-1-onto-> D <-> ( F : A -1-1-> C /\ G : C -1-1-onto-> D ) ) )
2 f1f1orn 
 |-  ( F : A -1-1-> C -> F : A -1-1-onto-> ran F )
3 f1oeq3 
 |-  ( ran F = C -> ( F : A -1-1-onto-> ran F <-> F : A -1-1-onto-> C ) )
4 2 3 syl5ib 
 |-  ( ran F = C -> ( F : A -1-1-> C -> F : A -1-1-onto-> C ) )
5 4 3ad2ant3 
 |-  ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> ( F : A -1-1-> C -> F : A -1-1-onto-> C ) )
6 f1of1 
 |-  ( F : A -1-1-onto-> C -> F : A -1-1-> C )
7 5 6 impbid1 
 |-  ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> ( F : A -1-1-> C <-> F : A -1-1-onto-> C ) )
8 7 anbi1d 
 |-  ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> ( ( F : A -1-1-> C /\ G : C -1-1-onto-> D ) <-> ( F : A -1-1-onto-> C /\ G : C -1-1-onto-> D ) ) )
9 1 8 bitrd 
 |-  ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> ( ( G o. F ) : A -1-1-onto-> D <-> ( F : A -1-1-onto-> C /\ G : C -1-1-onto-> D ) ) )