Metamath Proof Explorer

Theorem mapfien

Description: A bijection of the base sets induces a bijection on the set of finitely supported functions. (Contributed by Mario Carneiro, 30-May-2015) (Revised by AV, 3-Jul-2019)

Ref Expression
Hypotheses mapfien.s ⊢ 𝑆 = { 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) ∣ 𝑥 finSupp 𝑍 }
mapfien.t ⊢ 𝑇 = { 𝑥 ∈ ( 𝐷 ↑m 𝐶 ) ∣ 𝑥 finSupp 𝑊 }
mapfien.w ⊢ 𝑊 = ( 𝐺 ‘ 𝑍 )
mapfien.f ⊢ ( 𝜑 → 𝐹 : 𝐶 –1-1-onto→ 𝐴 )
mapfien.g ⊢ ( 𝜑 → 𝐺 : 𝐵 –1-1-onto→ 𝐷 )
mapfien.a ⊢ ( 𝜑 → 𝐴 ∈ V )
mapfien.b ⊢ ( 𝜑 → 𝐵 ∈ V )
mapfien.c ⊢ ( 𝜑 → 𝐶 ∈ V )
mapfien.d ⊢ ( 𝜑 → 𝐷 ∈ V )
mapfien.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
Assertion mapfien ( 𝜑 → ( 𝑓 ∈ 𝑆 ↦ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) : 𝑆 –1-1-onto→ 𝑇 )

Proof

Step Hyp Ref Expression
1 mapfien.s ⊢ 𝑆 = { 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) ∣ 𝑥 finSupp 𝑍 }
2 mapfien.t ⊢ 𝑇 = { 𝑥 ∈ ( 𝐷 ↑m 𝐶 ) ∣ 𝑥 finSupp 𝑊 }
3 mapfien.w ⊢ 𝑊 = ( 𝐺 ‘ 𝑍 )
4 mapfien.f ⊢ ( 𝜑 → 𝐹 : 𝐶 –1-1-onto→ 𝐴 )
5 mapfien.g ⊢ ( 𝜑 → 𝐺 : 𝐵 –1-1-onto→ 𝐷 )
6 mapfien.a ⊢ ( 𝜑 → 𝐴 ∈ V )
7 mapfien.b ⊢ ( 𝜑 → 𝐵 ∈ V )
8 mapfien.c ⊢ ( 𝜑 → 𝐶 ∈ V )
9 mapfien.d ⊢ ( 𝜑 → 𝐷 ∈ V )
10 mapfien.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
11 eqid ⊢ ( 𝑓 ∈ 𝑆 ↦ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) = ( 𝑓 ∈ 𝑆 ↦ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) )
12 f1of ⊢ ( 𝐺 : 𝐵 –1-1-onto→ 𝐷 → 𝐺 : 𝐵 ⟶ 𝐷 )
13 5 12 syl ⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐷 )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑆 ) → 𝐺 : 𝐵 ⟶ 𝐷 )
15 breq1 ⊢ ( 𝑥 = 𝑓 → ( 𝑥 finSupp 𝑍 ↔ 𝑓 finSupp 𝑍 ) )
16 15 1 elrab2 ⊢ ( 𝑓 ∈ 𝑆 ↔ ( 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑓 finSupp 𝑍 ) )
17 16 simplbi ⊢ ( 𝑓 ∈ 𝑆 → 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) )
18 17 adantl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑆 ) → 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) )
19 elmapi ⊢ ( 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) → 𝑓 : 𝐴 ⟶ 𝐵 )
20 18 19 syl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑆 ) → 𝑓 : 𝐴 ⟶ 𝐵 )
21 f1of ⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝐴 → 𝐹 : 𝐶 ⟶ 𝐴 )
22 4 21 syl ⊢ ( 𝜑 → 𝐹 : 𝐶 ⟶ 𝐴 )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑆 ) → 𝐹 : 𝐶 ⟶ 𝐴 )
24 fco ⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ 𝐹 : 𝐶 ⟶ 𝐴 ) → ( 𝑓 ∘ 𝐹 ) : 𝐶 ⟶ 𝐵 )
25 20 23 24 syl2anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑆 ) → ( 𝑓 ∘ 𝐹 ) : 𝐶 ⟶ 𝐵 )
26 fco ⊢ ( ( 𝐺 : 𝐵 ⟶ 𝐷 ∧ ( 𝑓 ∘ 𝐹 ) : 𝐶 ⟶ 𝐵 ) → ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) : 𝐶 ⟶ 𝐷 )
27 14 25 26 syl2anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑆 ) → ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) : 𝐶 ⟶ 𝐷 )
28 9 8 elmapd ⊢ ( 𝜑 → ( ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ∈ ( 𝐷 ↑m 𝐶 ) ↔ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) : 𝐶 ⟶ 𝐷 ) )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑆 ) → ( ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ∈ ( 𝐷 ↑m 𝐶 ) ↔ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) : 𝐶 ⟶ 𝐷 ) )
30 27 29 mpbird ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑆 ) → ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ∈ ( 𝐷 ↑m 𝐶 ) )
31 1 2 3 4 5 6 7 8 9 10 mapfienlem1 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑆 ) → ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) finSupp 𝑊 )
32 breq1 ⊢ ( 𝑥 = ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) → ( 𝑥 finSupp 𝑊 ↔ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) finSupp 𝑊 ) )
33 32 2 elrab2 ⊢ ( ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ∈ 𝑇 ↔ ( ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ∈ ( 𝐷 ↑m 𝐶 ) ∧ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) finSupp 𝑊 ) )
34 30 31 33 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑆 ) → ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ∈ 𝑇 )
35 1 2 3 4 5 6 7 8 9 10 mapfienlem3 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ∈ 𝑆 )
36 coass ⊢ ( ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ∘ 𝐹 ) = ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ( ◡ 𝐹 ∘ 𝐹 ) )
37 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → 𝐹 : 𝐶 –1-1-onto→ 𝐴 )
38 f1ococnv1 ⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝐴 → ( ◡ 𝐹 ∘ 𝐹 ) = ( I ↾ 𝐶 ) )
39 37 38 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ◡ 𝐹 ∘ 𝐹 ) = ( I ↾ 𝐶 ) )
40 39 coeq2d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ( ◡ 𝐹 ∘ 𝐹 ) ) = ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ( I ↾ 𝐶 ) ) )
41 f1ocnv ⊢ ( 𝐺 : 𝐵 –1-1-onto→ 𝐷 → ◡ 𝐺 : 𝐷 –1-1-onto→ 𝐵 )
42 f1of ⊢ ( ◡ 𝐺 : 𝐷 –1-1-onto→ 𝐵 → ◡ 𝐺 : 𝐷 ⟶ 𝐵 )
43 5 41 42 3syl ⊢ ( 𝜑 → ◡ 𝐺 : 𝐷 ⟶ 𝐵 )
44 43 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ◡ 𝐺 : 𝐷 ⟶ 𝐵 )
45 simpr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → 𝑔 ∈ 𝑇 )
46 breq1 ⊢ ( 𝑥 = 𝑔 → ( 𝑥 finSupp 𝑊 ↔ 𝑔 finSupp 𝑊 ) )
47 46 2 elrab2 ⊢ ( 𝑔 ∈ 𝑇 ↔ ( 𝑔 ∈ ( 𝐷 ↑m 𝐶 ) ∧ 𝑔 finSupp 𝑊 ) )
48 45 47 sylib ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ( 𝑔 ∈ ( 𝐷 ↑m 𝐶 ) ∧ 𝑔 finSupp 𝑊 ) )
49 48 simpld ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → 𝑔 ∈ ( 𝐷 ↑m 𝐶 ) )
50 elmapi ⊢ ( 𝑔 ∈ ( 𝐷 ↑m 𝐶 ) → 𝑔 : 𝐶 ⟶ 𝐷 )
51 49 50 syl ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → 𝑔 : 𝐶 ⟶ 𝐷 )
52 fco ⊢ ( ( ◡ 𝐺 : 𝐷 ⟶ 𝐵 ∧ 𝑔 : 𝐶 ⟶ 𝐷 ) → ( ◡ 𝐺 ∘ 𝑔 ) : 𝐶 ⟶ 𝐵 )
53 44 51 52 syl2anc ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ( ◡ 𝐺 ∘ 𝑔 ) : 𝐶 ⟶ 𝐵 )
54 53 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ◡ 𝐺 ∘ 𝑔 ) : 𝐶 ⟶ 𝐵 )
55 fcoi1 ⊢ ( ( ◡ 𝐺 ∘ 𝑔 ) : 𝐶 ⟶ 𝐵 → ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ( I ↾ 𝐶 ) ) = ( ◡ 𝐺 ∘ 𝑔 ) )
56 54 55 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ( I ↾ 𝐶 ) ) = ( ◡ 𝐺 ∘ 𝑔 ) )
57 40 56 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ( ◡ 𝐹 ∘ 𝐹 ) ) = ( ◡ 𝐺 ∘ 𝑔 ) )
58 36 57 syl5eq ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ∘ 𝐹 ) = ( ◡ 𝐺 ∘ 𝑔 ) )
59 58 eqeq2d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( 𝑓 ∘ 𝐹 ) = ( ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ∘ 𝐹 ) ↔ ( 𝑓 ∘ 𝐹 ) = ( ◡ 𝐺 ∘ 𝑔 ) ) )
60 coass ⊢ ( ( ◡ 𝐺 ∘ 𝐺 ) ∘ ( 𝑓 ∘ 𝐹 ) ) = ( ◡ 𝐺 ∘ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) )
61 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → 𝐺 : 𝐵 –1-1-onto→ 𝐷 )
62 f1ococnv1 ⊢ ( 𝐺 : 𝐵 –1-1-onto→ 𝐷 → ( ◡ 𝐺 ∘ 𝐺 ) = ( I ↾ 𝐵 ) )
63 61 62 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ◡ 𝐺 ∘ 𝐺 ) = ( I ↾ 𝐵 ) )
64 63 coeq1d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( ◡ 𝐺 ∘ 𝐺 ) ∘ ( 𝑓 ∘ 𝐹 ) ) = ( ( I ↾ 𝐵 ) ∘ ( 𝑓 ∘ 𝐹 ) ) )
65 25 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( 𝑓 ∘ 𝐹 ) : 𝐶 ⟶ 𝐵 )
66 fcoi2 ⊢ ( ( 𝑓 ∘ 𝐹 ) : 𝐶 ⟶ 𝐵 → ( ( I ↾ 𝐵 ) ∘ ( 𝑓 ∘ 𝐹 ) ) = ( 𝑓 ∘ 𝐹 ) )
67 65 66 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( I ↾ 𝐵 ) ∘ ( 𝑓 ∘ 𝐹 ) ) = ( 𝑓 ∘ 𝐹 ) )
68 64 67 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( ◡ 𝐺 ∘ 𝐺 ) ∘ ( 𝑓 ∘ 𝐹 ) ) = ( 𝑓 ∘ 𝐹 ) )
69 60 68 syl5eqr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ◡ 𝐺 ∘ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) = ( 𝑓 ∘ 𝐹 ) )
70 69 eqeq2d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( ◡ 𝐺 ∘ 𝑔 ) = ( ◡ 𝐺 ∘ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ↔ ( ◡ 𝐺 ∘ 𝑔 ) = ( 𝑓 ∘ 𝐹 ) ) )
71 eqcom ⊢ ( ( ◡ 𝐺 ∘ 𝑔 ) = ( 𝑓 ∘ 𝐹 ) ↔ ( 𝑓 ∘ 𝐹 ) = ( ◡ 𝐺 ∘ 𝑔 ) )
72 70 71 syl6bb ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( ◡ 𝐺 ∘ 𝑔 ) = ( ◡ 𝐺 ∘ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ↔ ( 𝑓 ∘ 𝐹 ) = ( ◡ 𝐺 ∘ 𝑔 ) ) )
73 59 72 bitr4d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( 𝑓 ∘ 𝐹 ) = ( ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ∘ 𝐹 ) ↔ ( ◡ 𝐺 ∘ 𝑔 ) = ( ◡ 𝐺 ∘ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ) )
74 f1ofo ⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝐴 → 𝐹 : 𝐶 –onto→ 𝐴 )
75 37 74 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → 𝐹 : 𝐶 –onto→ 𝐴 )
76 ffn ⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 → 𝑓 Fn 𝐴 )
77 18 19 76 3syl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑆 ) → 𝑓 Fn 𝐴 )
78 77 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → 𝑓 Fn 𝐴 )
79 f1ocnv ⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝐴 → ◡ 𝐹 : 𝐴 –1-1-onto→ 𝐶 )
80 f1of ⊢ ( ◡ 𝐹 : 𝐴 –1-1-onto→ 𝐶 → ◡ 𝐹 : 𝐴 ⟶ 𝐶 )
81 4 79 80 3syl ⊢ ( 𝜑 → ◡ 𝐹 : 𝐴 ⟶ 𝐶 )
82 81 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ◡ 𝐹 : 𝐴 ⟶ 𝐶 )
83 fco ⊢ ( ( ( ◡ 𝐺 ∘ 𝑔 ) : 𝐶 ⟶ 𝐵 ∧ ◡ 𝐹 : 𝐴 ⟶ 𝐶 ) → ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) : 𝐴 ⟶ 𝐵 )
84 53 82 83 syl2anc ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) : 𝐴 ⟶ 𝐵 )
85 84 ffnd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) Fn 𝐴 )
86 85 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) Fn 𝐴 )
87 cocan2 ⊢ ( ( 𝐹 : 𝐶 –onto→ 𝐴 ∧ 𝑓 Fn 𝐴 ∧ ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) Fn 𝐴 ) → ( ( 𝑓 ∘ 𝐹 ) = ( ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ∘ 𝐹 ) ↔ 𝑓 = ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ) )
88 75 78 86 87 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( 𝑓 ∘ 𝐹 ) = ( ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ∘ 𝐹 ) ↔ 𝑓 = ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ) )
89 5 41 syl ⊢ ( 𝜑 → ◡ 𝐺 : 𝐷 –1-1-onto→ 𝐵 )
90 89 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ◡ 𝐺 : 𝐷 –1-1-onto→ 𝐵 )
91 f1of1 ⊢ ( ◡ 𝐺 : 𝐷 –1-1-onto→ 𝐵 → ◡ 𝐺 : 𝐷 –1-1→ 𝐵 )
92 90 91 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ◡ 𝐺 : 𝐷 –1-1→ 𝐵 )
93 51 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → 𝑔 : 𝐶 ⟶ 𝐷 )
94 27 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) : 𝐶 ⟶ 𝐷 )
95 cocan1 ⊢ ( ( ◡ 𝐺 : 𝐷 –1-1→ 𝐵 ∧ 𝑔 : 𝐶 ⟶ 𝐷 ∧ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) : 𝐶 ⟶ 𝐷 ) → ( ( ◡ 𝐺 ∘ 𝑔 ) = ( ◡ 𝐺 ∘ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ↔ 𝑔 = ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) )
96 92 93 94 95 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( ◡ 𝐺 ∘ 𝑔 ) = ( ◡ 𝐺 ∘ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ↔ 𝑔 = ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) )
97 73 88 96 3bitr3d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( 𝑓 = ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ↔ 𝑔 = ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) )
98 11 34 35 97 f1o2d ⊢ ( 𝜑 → ( 𝑓 ∈ 𝑆 ↦ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) : 𝑆 –1-1-onto→ 𝑇 )