Metamath Proof Explorer

Theorem f1cof1b

Description: If the range of F equals the domain of G , then the composition ( G o. F ) is injective iff F and G are both injective. (Contributed by GL and AV, 19-Sep-2024)

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

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> F : A --> B )
2 eqid 
 |-  ( ran F i^i C ) = ( ran F i^i C )
3 eqid 
 |-  ( `' F " C ) = ( `' F " C )
4 eqid 
 |-  ( F |` ( `' F " C ) ) = ( F |` ( `' F " C ) )
5 simp2 
 |-  ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> G : C --> D )
6 eqid 
 |-  ( G |` ( ran F i^i C ) ) = ( G |` ( ran F i^i C ) )
7 simp3 
 |-  ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> ran F = C )
8 1 2 3 4 5 6 7 f1cof1blem 
 |-  ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> ( ( ( `' F " C ) = A /\ ( ran F i^i C ) = C ) /\ ( ( F |` ( `' F " C ) ) = F /\ ( G |` ( ran F i^i C ) ) = G ) ) )
9 simpll 
 |-  ( ( ( ( `' F " C ) = A /\ ( ran F i^i C ) = C ) /\ ( ( F |` ( `' F " C ) ) = F /\ ( G |` ( ran F i^i C ) ) = G ) ) -> ( `' F " C ) = A )
10 f1eq2 
 |-  ( ( `' F " C ) = A -> ( ( G o. F ) : ( `' F " C ) -1-1-> D <-> ( G o. F ) : A -1-1-> D ) )
11 8 9 10 3syl 
 |-  ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> ( ( G o. F ) : ( `' F " C ) -1-1-> D <-> ( G o. F ) : A -1-1-> D ) )
12 11 bicomd 
 |-  ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> ( ( G o. F ) : A -1-1-> D <-> ( G o. F ) : ( `' F " C ) -1-1-> D ) )
13 ancom 
 |-  ( ( ( G |` ( ran F i^i C ) ) = G /\ ( F |` ( `' F " C ) ) = F ) <-> ( ( F |` ( `' F " C ) ) = F /\ ( G |` ( ran F i^i C ) ) = G ) )
14 13 anbi2i 
 |-  ( ( ( ( `' F " C ) = A /\ ( ran F i^i C ) = C ) /\ ( ( G |` ( ran F i^i C ) ) = G /\ ( F |` ( `' F " C ) ) = F ) ) <-> ( ( ( `' F " C ) = A /\ ( ran F i^i C ) = C ) /\ ( ( F |` ( `' F " C ) ) = F /\ ( G |` ( ran F i^i C ) ) = G ) ) )
15 8 14 sylibr 
 |-  ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> ( ( ( `' F " C ) = A /\ ( ran F i^i C ) = C ) /\ ( ( G |` ( ran F i^i C ) ) = G /\ ( F |` ( `' F " C ) ) = F ) ) )
16 15 adantr 
 |-  ( ( ( F : A --> B /\ G : C --> D /\ ran F = C ) /\ ( G o. F ) : ( `' F " C ) -1-1-> D ) -> ( ( ( `' F " C ) = A /\ ( ran F i^i C ) = C ) /\ ( ( G |` ( ran F i^i C ) ) = G /\ ( F |` ( `' F " C ) ) = F ) ) )
17 1 adantr 
 |-  ( ( ( F : A --> B /\ G : C --> D /\ ran F = C ) /\ ( G o. F ) : ( `' F " C ) -1-1-> D ) -> F : A --> B )
18 5 adantr 
 |-  ( ( ( F : A --> B /\ G : C --> D /\ ran F = C ) /\ ( G o. F ) : ( `' F " C ) -1-1-> D ) -> G : C --> D )
19 simpr 
 |-  ( ( ( F : A --> B /\ G : C --> D /\ ran F = C ) /\ ( G o. F ) : ( `' F " C ) -1-1-> D ) -> ( G o. F ) : ( `' F " C ) -1-1-> D )
20 17 2 3 4 18 6 19 fcoresf1 
 |-  ( ( ( F : A --> B /\ G : C --> D /\ ran F = C ) /\ ( G o. F ) : ( `' F " C ) -1-1-> D ) -> ( ( F |` ( `' F " C ) ) : ( `' F " C ) -1-1-> ( ran F i^i C ) /\ ( G |` ( ran F i^i C ) ) : ( ran F i^i C ) -1-1-> D ) )
21 20 ancomd 
 |-  ( ( ( F : A --> B /\ G : C --> D /\ ran F = C ) /\ ( G o. F ) : ( `' F " C ) -1-1-> D ) -> ( ( G |` ( ran F i^i C ) ) : ( ran F i^i C ) -1-1-> D /\ ( F |` ( `' F " C ) ) : ( `' F " C ) -1-1-> ( ran F i^i C ) ) )
22 simprl 
 |-  ( ( ( ( `' F " C ) = A /\ ( ran F i^i C ) = C ) /\ ( ( G |` ( ran F i^i C ) ) = G /\ ( F |` ( `' F " C ) ) = F ) ) -> ( G |` ( ran F i^i C ) ) = G )
23 simpr 
 |-  ( ( ( `' F " C ) = A /\ ( ran F i^i C ) = C ) -> ( ran F i^i C ) = C )
24 23 adantr 
 |-  ( ( ( ( `' F " C ) = A /\ ( ran F i^i C ) = C ) /\ ( ( G |` ( ran F i^i C ) ) = G /\ ( F |` ( `' F " C ) ) = F ) ) -> ( ran F i^i C ) = C )
25 eqidd 
 |-  ( ( ( ( `' F " C ) = A /\ ( ran F i^i C ) = C ) /\ ( ( G |` ( ran F i^i C ) ) = G /\ ( F |` ( `' F " C ) ) = F ) ) -> D = D )
26 22 24 25 f1eq123d 
 |-  ( ( ( ( `' F " C ) = A /\ ( ran F i^i C ) = C ) /\ ( ( G |` ( ran F i^i C ) ) = G /\ ( F |` ( `' F " C ) ) = F ) ) -> ( ( G |` ( ran F i^i C ) ) : ( ran F i^i C ) -1-1-> D <-> G : C -1-1-> D ) )
27 26 biimpd 
 |-  ( ( ( ( `' F " C ) = A /\ ( ran F i^i C ) = C ) /\ ( ( G |` ( ran F i^i C ) ) = G /\ ( F |` ( `' F " C ) ) = F ) ) -> ( ( G |` ( ran F i^i C ) ) : ( ran F i^i C ) -1-1-> D -> G : C -1-1-> D ) )
28 simprr 
 |-  ( ( ( ( `' F " C ) = A /\ ( ran F i^i C ) = C ) /\ ( ( G |` ( ran F i^i C ) ) = G /\ ( F |` ( `' F " C ) ) = F ) ) -> ( F |` ( `' F " C ) ) = F )
29 simpll 
 |-  ( ( ( ( `' F " C ) = A /\ ( ran F i^i C ) = C ) /\ ( ( G |` ( ran F i^i C ) ) = G /\ ( F |` ( `' F " C ) ) = F ) ) -> ( `' F " C ) = A )
30 28 29 24 f1eq123d 
 |-  ( ( ( ( `' F " C ) = A /\ ( ran F i^i C ) = C ) /\ ( ( G |` ( ran F i^i C ) ) = G /\ ( F |` ( `' F " C ) ) = F ) ) -> ( ( F |` ( `' F " C ) ) : ( `' F " C ) -1-1-> ( ran F i^i C ) <-> F : A -1-1-> C ) )
31 30 biimpd 
 |-  ( ( ( ( `' F " C ) = A /\ ( ran F i^i C ) = C ) /\ ( ( G |` ( ran F i^i C ) ) = G /\ ( F |` ( `' F " C ) ) = F ) ) -> ( ( F |` ( `' F " C ) ) : ( `' F " C ) -1-1-> ( ran F i^i C ) -> F : A -1-1-> C ) )
32 27 31 anim12d 
 |-  ( ( ( ( `' F " C ) = A /\ ( ran F i^i C ) = C ) /\ ( ( G |` ( ran F i^i C ) ) = G /\ ( F |` ( `' F " C ) ) = F ) ) -> ( ( ( G |` ( ran F i^i C ) ) : ( ran F i^i C ) -1-1-> D /\ ( F |` ( `' F " C ) ) : ( `' F " C ) -1-1-> ( ran F i^i C ) ) -> ( G : C -1-1-> D /\ F : A -1-1-> C ) ) )
33 16 21 32 sylc 
 |-  ( ( ( F : A --> B /\ G : C --> D /\ ran F = C ) /\ ( G o. F ) : ( `' F " C ) -1-1-> D ) -> ( G : C -1-1-> D /\ F : A -1-1-> C ) )
34 12 33 sylbida 
 |-  ( ( ( F : A --> B /\ G : C --> D /\ ran F = C ) /\ ( G o. F ) : A -1-1-> D ) -> ( G : C -1-1-> D /\ F : A -1-1-> C ) )
35 ffrn 
 |-  ( F : A --> B -> F : A --> ran F )
36 ax-1 
 |-  ( F : A --> B -> ( F : A --> ran F -> F : A --> B ) )
37 35 36 impbid2 
 |-  ( F : A --> B -> ( F : A --> B <-> F : A --> ran F ) )
38 37 anbi1d 
 |-  ( F : A --> B -> ( ( F : A --> B /\ Fun `' F ) <-> ( F : A --> ran F /\ Fun `' F ) ) )
39 df-f1 
 |-  ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
40 df-f1 
 |-  ( F : A -1-1-> ran F <-> ( F : A --> ran F /\ Fun `' F ) )
41 38 39 40 3bitr4g 
 |-  ( F : A --> B -> ( F : A -1-1-> B <-> F : A -1-1-> ran F ) )
42 41 3ad2ant1 
 |-  ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> ( F : A -1-1-> B <-> F : A -1-1-> ran F ) )
43 f1eq3 
 |-  ( ran F = C -> ( F : A -1-1-> ran F <-> F : A -1-1-> C ) )
44 43 3ad2ant3 
 |-  ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> ( F : A -1-1-> ran F <-> F : A -1-1-> C ) )
45 42 44 bitrd 
 |-  ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> ( F : A -1-1-> B <-> F : A -1-1-> C ) )
46 45 anbi2d 
 |-  ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> ( ( G : C -1-1-> D /\ F : A -1-1-> B ) <-> ( G : C -1-1-> D /\ F : A -1-1-> C ) ) )
47 46 adantr 
 |-  ( ( ( F : A --> B /\ G : C --> D /\ ran F = C ) /\ ( G o. F ) : A -1-1-> D ) -> ( ( G : C -1-1-> D /\ F : A -1-1-> B ) <-> ( G : C -1-1-> D /\ F : A -1-1-> C ) ) )
48 34 47 mpbird 
 |-  ( ( ( F : A --> B /\ G : C --> D /\ ran F = C ) /\ ( G o. F ) : A -1-1-> D ) -> ( G : C -1-1-> D /\ F : A -1-1-> B ) )
49 48 ancomd 
 |-  ( ( ( F : A --> B /\ G : C --> D /\ ran F = C ) /\ ( G o. F ) : A -1-1-> D ) -> ( F : A -1-1-> B /\ G : C -1-1-> D ) )
50 49 ex 
 |-  ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> ( ( G o. F ) : A -1-1-> D -> ( F : A -1-1-> B /\ G : C -1-1-> D ) ) )
51 f1cof1 
 |-  ( ( G : C -1-1-> D /\ F : A -1-1-> B ) -> ( G o. F ) : ( `' F " C ) -1-1-> D )
52 51 ancoms 
 |-  ( ( F : A -1-1-> B /\ G : C -1-1-> D ) -> ( G o. F ) : ( `' F " C ) -1-1-> D )
53 imaeq2 
 |-  ( C = ran F -> ( `' F " C ) = ( `' F " ran F ) )
54 cnvimarndm 
 |-  ( `' F " ran F ) = dom F
55 53 54 eqtrdi 
 |-  ( C = ran F -> ( `' F " C ) = dom F )
56 55 eqcoms 
 |-  ( ran F = C -> ( `' F " C ) = dom F )
57 56 3ad2ant3 
 |-  ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> ( `' F " C ) = dom F )
58 1 fdmd 
 |-  ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> dom F = A )
59 57 58 eqtrd 
 |-  ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> ( `' F " C ) = A )
60 59 10 syl 
 |-  ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> ( ( G o. F ) : ( `' F " C ) -1-1-> D <-> ( G o. F ) : A -1-1-> D ) )
61 52 60 syl5ib 
 |-  ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> ( ( F : A -1-1-> B /\ G : C -1-1-> D ) -> ( G o. F ) : A -1-1-> D ) )
62 50 61 impbid 
 |-  ( ( F : A --> B /\ G : C --> D /\ ran F = C ) -> ( ( G o. F ) : A -1-1-> D <-> ( F : A -1-1-> B /\ G : C -1-1-> D ) ) )