Metamath Proof Explorer

Theorem f1ocof1ob

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. (Contributed by GL and AV, 7-Oct-2024)

Ref Expression
Assertion 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 ) ) )

Proof

Step Hyp Ref Expression
1 ffrn 
 |-  ( F : A --> B -> F : A --> ran F )
2 1 3ad2ant1 
 |-  ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> F : A --> ran F )
3 feq3 
 |-  ( ran F = C -> ( F : A --> ran F <-> F : A --> C ) )
4 3 3ad2ant3 
 |-  ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> ( F : A --> ran F <-> F : A --> C ) )
5 2 4 mpbid 
 |-  ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> F : A --> C )
6 f1cof1b 
 |-  ( ( F : A --> C /\ G : C --> D /\ ran F = C ) -> ( ( G o. F ) : A -1-1-> D <-> ( F : A -1-1-> C /\ G : C -1-1-> D ) ) )
7 5 6 syld3an1 
 |-  ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> ( ( G o. F ) : A -1-1-> D <-> ( F : A -1-1-> C /\ G : C -1-1-> D ) ) )
8 ffn 
 |-  ( F : A --> B -> F Fn A )
9 fnfocofob 
 |-  ( ( F Fn A /\ G : C --> D /\ ran F = C ) -> ( ( G o. F ) : A -onto-> D <-> G : C -onto-> D ) )
10 8 9 syl3an1 
 |-  ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> ( ( G o. F ) : A -onto-> D <-> G : C -onto-> D ) )
11 7 10 anbi12d 
 |-  ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> ( ( ( G o. F ) : A -1-1-> D /\ ( G o. F ) : A -onto-> D ) <-> ( ( F : A -1-1-> C /\ G : C -1-1-> D ) /\ G : C -onto-> D ) ) )
12 anass 
 |-  ( ( ( F : A -1-1-> C /\ G : C -1-1-> D ) /\ G : C -onto-> D ) <-> ( F : A -1-1-> C /\ ( G : C -1-1-> D /\ G : C -onto-> D ) ) )
13 11 12 bitrdi 
 |-  ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> ( ( ( G o. F ) : A -1-1-> D /\ ( G o. F ) : A -onto-> D ) <-> ( F : A -1-1-> C /\ ( G : C -1-1-> D /\ G : C -onto-> D ) ) ) )
14 df-f1o 
 |-  ( ( G o. F ) : A -1-1-onto-> D <-> ( ( G o. F ) : A -1-1-> D /\ ( G o. F ) : A -onto-> D ) )
15 df-f1o 
 |-  ( G : C -1-1-onto-> D <-> ( G : C -1-1-> D /\ G : C -onto-> D ) )
16 15 anbi2i 
 |-  ( ( F : A -1-1-> C /\ G : C -1-1-onto-> D ) <-> ( F : A -1-1-> C /\ ( G : C -1-1-> D /\ G : C -onto-> D ) ) )
17 13 14 16 3bitr4g 
 |-  ( ( 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 ) ) )