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 ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) → ( ( 𝐺 ∘ 𝐹 ) : 𝐴 –1-1→ 𝐷 ↔ ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐶 –1-1→ 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
2 eqid ⊢ ( ran 𝐹 ∩ 𝐶 ) = ( ran 𝐹 ∩ 𝐶 )
3 eqid ⊢ ( ◡ 𝐹 “ 𝐶 ) = ( ◡ 𝐹 “ 𝐶 )
4 eqid ⊢ ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) = ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) )
5 simp2 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) → 𝐺 : 𝐶 ⟶ 𝐷 )
6 eqid ⊢ ( 𝐺 ↾ ( ran 𝐹 ∩ 𝐶 ) ) = ( 𝐺 ↾ ( ran 𝐹 ∩ 𝐶 ) )
7 simp3 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) → ran 𝐹 = 𝐶 )
8 1 2 3 4 5 6 7 f1cof1blem ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) → ( ( ( ◡ 𝐹 “ 𝐶 ) = 𝐴 ∧ ( ran 𝐹 ∩ 𝐶 ) = 𝐶 ) ∧ ( ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) = 𝐹 ∧ ( 𝐺 ↾ ( ran 𝐹 ∩ 𝐶 ) ) = 𝐺 ) ) )
9 simpll ⊢ ( ( ( ( ◡ 𝐹 “ 𝐶 ) = 𝐴 ∧ ( ran 𝐹 ∩ 𝐶 ) = 𝐶 ) ∧ ( ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) = 𝐹 ∧ ( 𝐺 ↾ ( ran 𝐹 ∩ 𝐶 ) ) = 𝐺 ) ) → ( ◡ 𝐹 “ 𝐶 ) = 𝐴 )
10 f1eq2 ⊢ ( ( ◡ 𝐹 “ 𝐶 ) = 𝐴 → ( ( 𝐺 ∘ 𝐹 ) : ( ◡ 𝐹 “ 𝐶 ) –1-1→ 𝐷 ↔ ( 𝐺 ∘ 𝐹 ) : 𝐴 –1-1→ 𝐷 ) )
11 8 9 10 3syl ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) → ( ( 𝐺 ∘ 𝐹 ) : ( ◡ 𝐹 “ 𝐶 ) –1-1→ 𝐷 ↔ ( 𝐺 ∘ 𝐹 ) : 𝐴 –1-1→ 𝐷 ) )
12 11 bicomd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) → ( ( 𝐺 ∘ 𝐹 ) : 𝐴 –1-1→ 𝐷 ↔ ( 𝐺 ∘ 𝐹 ) : ( ◡ 𝐹 “ 𝐶 ) –1-1→ 𝐷 ) )
13 ancom ⊢ ( ( ( 𝐺 ↾ ( ran 𝐹 ∩ 𝐶 ) ) = 𝐺 ∧ ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) = 𝐹 ) ↔ ( ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) = 𝐹 ∧ ( 𝐺 ↾ ( ran 𝐹 ∩ 𝐶 ) ) = 𝐺 ) )
14 13 anbi2i ⊢ ( ( ( ( ◡ 𝐹 “ 𝐶 ) = 𝐴 ∧ ( ran 𝐹 ∩ 𝐶 ) = 𝐶 ) ∧ ( ( 𝐺 ↾ ( ran 𝐹 ∩ 𝐶 ) ) = 𝐺 ∧ ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) = 𝐹 ) ) ↔ ( ( ( ◡ 𝐹 “ 𝐶 ) = 𝐴 ∧ ( ran 𝐹 ∩ 𝐶 ) = 𝐶 ) ∧ ( ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) = 𝐹 ∧ ( 𝐺 ↾ ( ran 𝐹 ∩ 𝐶 ) ) = 𝐺 ) ) )
15 8 14 sylibr ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) → ( ( ( ◡ 𝐹 “ 𝐶 ) = 𝐴 ∧ ( ran 𝐹 ∩ 𝐶 ) = 𝐶 ) ∧ ( ( 𝐺 ↾ ( ran 𝐹 ∩ 𝐶 ) ) = 𝐺 ∧ ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) = 𝐹 ) ) )
16 15 adantr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) ∧ ( 𝐺 ∘ 𝐹 ) : ( ◡ 𝐹 “ 𝐶 ) –1-1→ 𝐷 ) → ( ( ( ◡ 𝐹 “ 𝐶 ) = 𝐴 ∧ ( ran 𝐹 ∩ 𝐶 ) = 𝐶 ) ∧ ( ( 𝐺 ↾ ( ran 𝐹 ∩ 𝐶 ) ) = 𝐺 ∧ ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) = 𝐹 ) ) )
17 1 adantr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) ∧ ( 𝐺 ∘ 𝐹 ) : ( ◡ 𝐹 “ 𝐶 ) –1-1→ 𝐷 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
18 5 adantr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) ∧ ( 𝐺 ∘ 𝐹 ) : ( ◡ 𝐹 “ 𝐶 ) –1-1→ 𝐷 ) → 𝐺 : 𝐶 ⟶ 𝐷 )
19 simpr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) ∧ ( 𝐺 ∘ 𝐹 ) : ( ◡ 𝐹 “ 𝐶 ) –1-1→ 𝐷 ) → ( 𝐺 ∘ 𝐹 ) : ( ◡ 𝐹 “ 𝐶 ) –1-1→ 𝐷 )
20 17 2 3 4 18 6 19 fcoresf1 ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) ∧ ( 𝐺 ∘ 𝐹 ) : ( ◡ 𝐹 “ 𝐶 ) –1-1→ 𝐷 ) → ( ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) : ( ◡ 𝐹 “ 𝐶 ) –1-1→ ( ran 𝐹 ∩ 𝐶 ) ∧ ( 𝐺 ↾ ( ran 𝐹 ∩ 𝐶 ) ) : ( ran 𝐹 ∩ 𝐶 ) –1-1→ 𝐷 ) )
21 20 ancomd ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) ∧ ( 𝐺 ∘ 𝐹 ) : ( ◡ 𝐹 “ 𝐶 ) –1-1→ 𝐷 ) → ( ( 𝐺 ↾ ( ran 𝐹 ∩ 𝐶 ) ) : ( ran 𝐹 ∩ 𝐶 ) –1-1→ 𝐷 ∧ ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) : ( ◡ 𝐹 “ 𝐶 ) –1-1→ ( ran 𝐹 ∩ 𝐶 ) ) )
22 simprl ⊢ ( ( ( ( ◡ 𝐹 “ 𝐶 ) = 𝐴 ∧ ( ran 𝐹 ∩ 𝐶 ) = 𝐶 ) ∧ ( ( 𝐺 ↾ ( ran 𝐹 ∩ 𝐶 ) ) = 𝐺 ∧ ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) = 𝐹 ) ) → ( 𝐺 ↾ ( ran 𝐹 ∩ 𝐶 ) ) = 𝐺 )
23 simpr ⊢ ( ( ( ◡ 𝐹 “ 𝐶 ) = 𝐴 ∧ ( ran 𝐹 ∩ 𝐶 ) = 𝐶 ) → ( ran 𝐹 ∩ 𝐶 ) = 𝐶 )
24 23 adantr ⊢ ( ( ( ( ◡ 𝐹 “ 𝐶 ) = 𝐴 ∧ ( ran 𝐹 ∩ 𝐶 ) = 𝐶 ) ∧ ( ( 𝐺 ↾ ( ran 𝐹 ∩ 𝐶 ) ) = 𝐺 ∧ ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) = 𝐹 ) ) → ( ran 𝐹 ∩ 𝐶 ) = 𝐶 )
25 eqidd ⊢ ( ( ( ( ◡ 𝐹 “ 𝐶 ) = 𝐴 ∧ ( ran 𝐹 ∩ 𝐶 ) = 𝐶 ) ∧ ( ( 𝐺 ↾ ( ran 𝐹 ∩ 𝐶 ) ) = 𝐺 ∧ ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) = 𝐹 ) ) → 𝐷 = 𝐷 )
26 22 24 25 f1eq123d ⊢ ( ( ( ( ◡ 𝐹 “ 𝐶 ) = 𝐴 ∧ ( ran 𝐹 ∩ 𝐶 ) = 𝐶 ) ∧ ( ( 𝐺 ↾ ( ran 𝐹 ∩ 𝐶 ) ) = 𝐺 ∧ ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) = 𝐹 ) ) → ( ( 𝐺 ↾ ( ran 𝐹 ∩ 𝐶 ) ) : ( ran 𝐹 ∩ 𝐶 ) –1-1→ 𝐷 ↔ 𝐺 : 𝐶 –1-1→ 𝐷 ) )
27 26 biimpd ⊢ ( ( ( ( ◡ 𝐹 “ 𝐶 ) = 𝐴 ∧ ( ran 𝐹 ∩ 𝐶 ) = 𝐶 ) ∧ ( ( 𝐺 ↾ ( ran 𝐹 ∩ 𝐶 ) ) = 𝐺 ∧ ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) = 𝐹 ) ) → ( ( 𝐺 ↾ ( ran 𝐹 ∩ 𝐶 ) ) : ( ran 𝐹 ∩ 𝐶 ) –1-1→ 𝐷 → 𝐺 : 𝐶 –1-1→ 𝐷 ) )
28 simprr ⊢ ( ( ( ( ◡ 𝐹 “ 𝐶 ) = 𝐴 ∧ ( ran 𝐹 ∩ 𝐶 ) = 𝐶 ) ∧ ( ( 𝐺 ↾ ( ran 𝐹 ∩ 𝐶 ) ) = 𝐺 ∧ ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) = 𝐹 ) ) → ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) = 𝐹 )
29 simpll ⊢ ( ( ( ( ◡ 𝐹 “ 𝐶 ) = 𝐴 ∧ ( ran 𝐹 ∩ 𝐶 ) = 𝐶 ) ∧ ( ( 𝐺 ↾ ( ran 𝐹 ∩ 𝐶 ) ) = 𝐺 ∧ ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) = 𝐹 ) ) → ( ◡ 𝐹 “ 𝐶 ) = 𝐴 )
30 28 29 24 f1eq123d ⊢ ( ( ( ( ◡ 𝐹 “ 𝐶 ) = 𝐴 ∧ ( ran 𝐹 ∩ 𝐶 ) = 𝐶 ) ∧ ( ( 𝐺 ↾ ( ran 𝐹 ∩ 𝐶 ) ) = 𝐺 ∧ ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) = 𝐹 ) ) → ( ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) : ( ◡ 𝐹 “ 𝐶 ) –1-1→ ( ran 𝐹 ∩ 𝐶 ) ↔ 𝐹 : 𝐴 –1-1→ 𝐶 ) )
31 30 biimpd ⊢ ( ( ( ( ◡ 𝐹 “ 𝐶 ) = 𝐴 ∧ ( ran 𝐹 ∩ 𝐶 ) = 𝐶 ) ∧ ( ( 𝐺 ↾ ( ran 𝐹 ∩ 𝐶 ) ) = 𝐺 ∧ ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) = 𝐹 ) ) → ( ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) : ( ◡ 𝐹 “ 𝐶 ) –1-1→ ( ran 𝐹 ∩ 𝐶 ) → 𝐹 : 𝐴 –1-1→ 𝐶 ) )
32 27 31 anim12d ⊢ ( ( ( ( ◡ 𝐹 “ 𝐶 ) = 𝐴 ∧ ( ran 𝐹 ∩ 𝐶 ) = 𝐶 ) ∧ ( ( 𝐺 ↾ ( ran 𝐹 ∩ 𝐶 ) ) = 𝐺 ∧ ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) = 𝐹 ) ) → ( ( ( 𝐺 ↾ ( ran 𝐹 ∩ 𝐶 ) ) : ( ran 𝐹 ∩ 𝐶 ) –1-1→ 𝐷 ∧ ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) : ( ◡ 𝐹 “ 𝐶 ) –1-1→ ( ran 𝐹 ∩ 𝐶 ) ) → ( 𝐺 : 𝐶 –1-1→ 𝐷 ∧ 𝐹 : 𝐴 –1-1→ 𝐶 ) ) )
33 16 21 32 sylc ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) ∧ ( 𝐺 ∘ 𝐹 ) : ( ◡ 𝐹 “ 𝐶 ) –1-1→ 𝐷 ) → ( 𝐺 : 𝐶 –1-1→ 𝐷 ∧ 𝐹 : 𝐴 –1-1→ 𝐶 ) )
34 12 33 sylbida ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) ∧ ( 𝐺 ∘ 𝐹 ) : 𝐴 –1-1→ 𝐷 ) → ( 𝐺 : 𝐶 –1-1→ 𝐷 ∧ 𝐹 : 𝐴 –1-1→ 𝐶 ) )
35 ffrn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 : 𝐴 ⟶ ran 𝐹 )
36 ax-1 ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 : 𝐴 ⟶ ran 𝐹 → 𝐹 : 𝐴 ⟶ 𝐵 ) )
37 35 36 impbid2 ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ 𝐹 : 𝐴 ⟶ ran 𝐹 ) )
38 37 anbi1d ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Fun ◡ 𝐹 ) ↔ ( 𝐹 : 𝐴 ⟶ ran 𝐹 ∧ Fun ◡ 𝐹 ) ) )
39 df-f1 ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Fun ◡ 𝐹 ) )
40 df-f1 ⊢ ( 𝐹 : 𝐴 –1-1→ ran 𝐹 ↔ ( 𝐹 : 𝐴 ⟶ ran 𝐹 ∧ Fun ◡ 𝐹 ) )
41 38 39 40 3bitr4g ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ 𝐹 : 𝐴 –1-1→ ran 𝐹 ) )
42 41 3ad2ant1 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ 𝐹 : 𝐴 –1-1→ ran 𝐹 ) )
43 f1eq3 ⊢ ( ran 𝐹 = 𝐶 → ( 𝐹 : 𝐴 –1-1→ ran 𝐹 ↔ 𝐹 : 𝐴 –1-1→ 𝐶 ) )
44 43 3ad2ant3 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) → ( 𝐹 : 𝐴 –1-1→ ran 𝐹 ↔ 𝐹 : 𝐴 –1-1→ 𝐶 ) )
45 42 44 bitrd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ 𝐹 : 𝐴 –1-1→ 𝐶 ) )
46 45 anbi2d ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) → ( ( 𝐺 : 𝐶 –1-1→ 𝐷 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) ↔ ( 𝐺 : 𝐶 –1-1→ 𝐷 ∧ 𝐹 : 𝐴 –1-1→ 𝐶 ) ) )
47 46 adantr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) ∧ ( 𝐺 ∘ 𝐹 ) : 𝐴 –1-1→ 𝐷 ) → ( ( 𝐺 : 𝐶 –1-1→ 𝐷 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) ↔ ( 𝐺 : 𝐶 –1-1→ 𝐷 ∧ 𝐹 : 𝐴 –1-1→ 𝐶 ) ) )
48 34 47 mpbird ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) ∧ ( 𝐺 ∘ 𝐹 ) : 𝐴 –1-1→ 𝐷 ) → ( 𝐺 : 𝐶 –1-1→ 𝐷 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) )
49 48 ancomd ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) ∧ ( 𝐺 ∘ 𝐹 ) : 𝐴 –1-1→ 𝐷 ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐶 –1-1→ 𝐷 ) )
50 49 ex ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) → ( ( 𝐺 ∘ 𝐹 ) : 𝐴 –1-1→ 𝐷 → ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐶 –1-1→ 𝐷 ) ) )
51 f1cof1 ⊢ ( ( 𝐺 : 𝐶 –1-1→ 𝐷 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( 𝐺 ∘ 𝐹 ) : ( ◡ 𝐹 “ 𝐶 ) –1-1→ 𝐷 )
52 51 ancoms ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐶 –1-1→ 𝐷 ) → ( 𝐺 ∘ 𝐹 ) : ( ◡ 𝐹 “ 𝐶 ) –1-1→ 𝐷 )
53 imaeq2 ⊢ ( 𝐶 = ran 𝐹 → ( ◡ 𝐹 “ 𝐶 ) = ( ◡ 𝐹 “ ran 𝐹 ) )
54 cnvimarndm ⊢ ( ◡ 𝐹 “ ran 𝐹 ) = dom 𝐹
55 53 54 eqtrdi ⊢ ( 𝐶 = ran 𝐹 → ( ◡ 𝐹 “ 𝐶 ) = dom 𝐹 )
56 55 eqcoms ⊢ ( ran 𝐹 = 𝐶 → ( ◡ 𝐹 “ 𝐶 ) = dom 𝐹 )
57 56 3ad2ant3 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) → ( ◡ 𝐹 “ 𝐶 ) = dom 𝐹 )
58 1 fdmd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) → dom 𝐹 = 𝐴 )
59 57 58 eqtrd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) → ( ◡ 𝐹 “ 𝐶 ) = 𝐴 )
60 59 10 syl ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) → ( ( 𝐺 ∘ 𝐹 ) : ( ◡ 𝐹 “ 𝐶 ) –1-1→ 𝐷 ↔ ( 𝐺 ∘ 𝐹 ) : 𝐴 –1-1→ 𝐷 ) )
61 52 60 imbitrid ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) → ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐶 –1-1→ 𝐷 ) → ( 𝐺 ∘ 𝐹 ) : 𝐴 –1-1→ 𝐷 ) )
62 50 61 impbid ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐶 ⟶ 𝐷 ∧ ran 𝐹 = 𝐶 ) → ( ( 𝐺 ∘ 𝐹 ) : 𝐴 –1-1→ 𝐷 ↔ ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐺 : 𝐶 –1-1→ 𝐷 ) ) )