This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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) (Revised by AV, 28-Jul-2024)

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 ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
mapfien.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
mapfien.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
mapfien.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑌 )
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 ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
7 mapfien.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
8 mapfien.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
9 mapfien.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑌 )
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 20 23 fcod ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑆 ) → ( 𝑓 ∘ 𝐹 ) : 𝐶 ⟶ 𝐵 )
25 14 24 fcod ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑆 ) → ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) : 𝐶 ⟶ 𝐷 )
26 9 8 elmapd ⊢ ( 𝜑 → ( ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ∈ ( 𝐷 ↑m 𝐶 ) ↔ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) : 𝐶 ⟶ 𝐷 ) )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑆 ) → ( ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ∈ ( 𝐷 ↑m 𝐶 ) ↔ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) : 𝐶 ⟶ 𝐷 ) )
28 25 27 mpbird ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑆 ) → ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ∈ ( 𝐷 ↑m 𝐶 ) )
29 1 2 3 4 5 6 7 8 9 10 mapfienlem1 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑆 ) → ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) finSupp 𝑊 )
30 breq1 ⊢ ( 𝑥 = ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) → ( 𝑥 finSupp 𝑊 ↔ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) finSupp 𝑊 ) )
31 30 2 elrab2 ⊢ ( ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ∈ 𝑇 ↔ ( ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ∈ ( 𝐷 ↑m 𝐶 ) ∧ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) finSupp 𝑊 ) )
32 28 29 31 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑆 ) → ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ∈ 𝑇 )
33 1 2 3 4 5 6 7 8 9 10 mapfienlem3 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ∈ 𝑆 )
34 coass ⊢ ( ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ∘ 𝐹 ) = ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ( ◡ 𝐹 ∘ 𝐹 ) )
35 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → 𝐹 : 𝐶 –1-1-onto→ 𝐴 )
36 f1ococnv1 ⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝐴 → ( ◡ 𝐹 ∘ 𝐹 ) = ( I ↾ 𝐶 ) )
37 35 36 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ◡ 𝐹 ∘ 𝐹 ) = ( I ↾ 𝐶 ) )
38 37 coeq2d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ( ◡ 𝐹 ∘ 𝐹 ) ) = ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ( I ↾ 𝐶 ) ) )
39 f1ocnv ⊢ ( 𝐺 : 𝐵 –1-1-onto→ 𝐷 → ◡ 𝐺 : 𝐷 –1-1-onto→ 𝐵 )
40 f1of ⊢ ( ◡ 𝐺 : 𝐷 –1-1-onto→ 𝐵 → ◡ 𝐺 : 𝐷 ⟶ 𝐵 )
41 5 39 40 3syl ⊢ ( 𝜑 → ◡ 𝐺 : 𝐷 ⟶ 𝐵 )
42 41 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ◡ 𝐺 : 𝐷 ⟶ 𝐵 )
43 simpr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → 𝑔 ∈ 𝑇 )
44 breq1 ⊢ ( 𝑥 = 𝑔 → ( 𝑥 finSupp 𝑊 ↔ 𝑔 finSupp 𝑊 ) )
45 44 2 elrab2 ⊢ ( 𝑔 ∈ 𝑇 ↔ ( 𝑔 ∈ ( 𝐷 ↑m 𝐶 ) ∧ 𝑔 finSupp 𝑊 ) )
46 43 45 sylib ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ( 𝑔 ∈ ( 𝐷 ↑m 𝐶 ) ∧ 𝑔 finSupp 𝑊 ) )
47 46 simpld ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → 𝑔 ∈ ( 𝐷 ↑m 𝐶 ) )
48 elmapi ⊢ ( 𝑔 ∈ ( 𝐷 ↑m 𝐶 ) → 𝑔 : 𝐶 ⟶ 𝐷 )
49 47 48 syl ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → 𝑔 : 𝐶 ⟶ 𝐷 )
50 42 49 fcod ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ( ◡ 𝐺 ∘ 𝑔 ) : 𝐶 ⟶ 𝐵 )
51 50 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ◡ 𝐺 ∘ 𝑔 ) : 𝐶 ⟶ 𝐵 )
52 fcoi1 ⊢ ( ( ◡ 𝐺 ∘ 𝑔 ) : 𝐶 ⟶ 𝐵 → ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ( I ↾ 𝐶 ) ) = ( ◡ 𝐺 ∘ 𝑔 ) )
53 51 52 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ( I ↾ 𝐶 ) ) = ( ◡ 𝐺 ∘ 𝑔 ) )
54 38 53 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ( ◡ 𝐹 ∘ 𝐹 ) ) = ( ◡ 𝐺 ∘ 𝑔 ) )
55 34 54 eqtrid ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ∘ 𝐹 ) = ( ◡ 𝐺 ∘ 𝑔 ) )
56 55 eqeq2d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( 𝑓 ∘ 𝐹 ) = ( ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ∘ 𝐹 ) ↔ ( 𝑓 ∘ 𝐹 ) = ( ◡ 𝐺 ∘ 𝑔 ) ) )
57 coass ⊢ ( ( ◡ 𝐺 ∘ 𝐺 ) ∘ ( 𝑓 ∘ 𝐹 ) ) = ( ◡ 𝐺 ∘ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) )
58 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → 𝐺 : 𝐵 –1-1-onto→ 𝐷 )
59 f1ococnv1 ⊢ ( 𝐺 : 𝐵 –1-1-onto→ 𝐷 → ( ◡ 𝐺 ∘ 𝐺 ) = ( I ↾ 𝐵 ) )
60 58 59 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ◡ 𝐺 ∘ 𝐺 ) = ( I ↾ 𝐵 ) )
61 60 coeq1d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( ◡ 𝐺 ∘ 𝐺 ) ∘ ( 𝑓 ∘ 𝐹 ) ) = ( ( I ↾ 𝐵 ) ∘ ( 𝑓 ∘ 𝐹 ) ) )
62 24 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( 𝑓 ∘ 𝐹 ) : 𝐶 ⟶ 𝐵 )
63 fcoi2 ⊢ ( ( 𝑓 ∘ 𝐹 ) : 𝐶 ⟶ 𝐵 → ( ( I ↾ 𝐵 ) ∘ ( 𝑓 ∘ 𝐹 ) ) = ( 𝑓 ∘ 𝐹 ) )
64 62 63 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( I ↾ 𝐵 ) ∘ ( 𝑓 ∘ 𝐹 ) ) = ( 𝑓 ∘ 𝐹 ) )
65 61 64 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( ◡ 𝐺 ∘ 𝐺 ) ∘ ( 𝑓 ∘ 𝐹 ) ) = ( 𝑓 ∘ 𝐹 ) )
66 57 65 eqtr3id ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ◡ 𝐺 ∘ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) = ( 𝑓 ∘ 𝐹 ) )
67 66 eqeq2d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( ◡ 𝐺 ∘ 𝑔 ) = ( ◡ 𝐺 ∘ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ↔ ( ◡ 𝐺 ∘ 𝑔 ) = ( 𝑓 ∘ 𝐹 ) ) )
68 eqcom ⊢ ( ( ◡ 𝐺 ∘ 𝑔 ) = ( 𝑓 ∘ 𝐹 ) ↔ ( 𝑓 ∘ 𝐹 ) = ( ◡ 𝐺 ∘ 𝑔 ) )
69 67 68 bitrdi ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( ◡ 𝐺 ∘ 𝑔 ) = ( ◡ 𝐺 ∘ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ↔ ( 𝑓 ∘ 𝐹 ) = ( ◡ 𝐺 ∘ 𝑔 ) ) )
70 56 69 bitr4d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( 𝑓 ∘ 𝐹 ) = ( ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ∘ 𝐹 ) ↔ ( ◡ 𝐺 ∘ 𝑔 ) = ( ◡ 𝐺 ∘ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ) )
71 f1ofo ⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝐴 → 𝐹 : 𝐶 –onto→ 𝐴 )
72 35 71 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → 𝐹 : 𝐶 –onto→ 𝐴 )
73 ffn ⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 → 𝑓 Fn 𝐴 )
74 18 19 73 3syl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑆 ) → 𝑓 Fn 𝐴 )
75 74 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → 𝑓 Fn 𝐴 )
76 f1ocnv ⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝐴 → ◡ 𝐹 : 𝐴 –1-1-onto→ 𝐶 )
77 f1of ⊢ ( ◡ 𝐹 : 𝐴 –1-1-onto→ 𝐶 → ◡ 𝐹 : 𝐴 ⟶ 𝐶 )
78 4 76 77 3syl ⊢ ( 𝜑 → ◡ 𝐹 : 𝐴 ⟶ 𝐶 )
79 78 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ◡ 𝐹 : 𝐴 ⟶ 𝐶 )
80 50 79 fcod ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) : 𝐴 ⟶ 𝐵 )
81 80 ffnd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) Fn 𝐴 )
82 81 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) Fn 𝐴 )
83 cocan2 ⊢ ( ( 𝐹 : 𝐶 –onto→ 𝐴 ∧ 𝑓 Fn 𝐴 ∧ ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) Fn 𝐴 ) → ( ( 𝑓 ∘ 𝐹 ) = ( ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ∘ 𝐹 ) ↔ 𝑓 = ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ) )
84 72 75 82 83 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( 𝑓 ∘ 𝐹 ) = ( ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ∘ 𝐹 ) ↔ 𝑓 = ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ) )
85 5 39 syl ⊢ ( 𝜑 → ◡ 𝐺 : 𝐷 –1-1-onto→ 𝐵 )
86 85 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ◡ 𝐺 : 𝐷 –1-1-onto→ 𝐵 )
87 f1of1 ⊢ ( ◡ 𝐺 : 𝐷 –1-1-onto→ 𝐵 → ◡ 𝐺 : 𝐷 –1-1→ 𝐵 )
88 86 87 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ◡ 𝐺 : 𝐷 –1-1→ 𝐵 )
89 49 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → 𝑔 : 𝐶 ⟶ 𝐷 )
90 25 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) : 𝐶 ⟶ 𝐷 )
91 cocan1 ⊢ ( ( ◡ 𝐺 : 𝐷 –1-1→ 𝐵 ∧ 𝑔 : 𝐶 ⟶ 𝐷 ∧ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) : 𝐶 ⟶ 𝐷 ) → ( ( ◡ 𝐺 ∘ 𝑔 ) = ( ◡ 𝐺 ∘ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ↔ 𝑔 = ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) )
92 88 89 90 91 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( ◡ 𝐺 ∘ 𝑔 ) = ( ◡ 𝐺 ∘ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ↔ 𝑔 = ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) )
93 70 84 92 3bitr3d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( 𝑓 = ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ↔ 𝑔 = ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) )
94 11 32 33 93 f1o2d ⊢ ( 𝜑 → ( 𝑓 ∈ 𝑆 ↦ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) : 𝑆 –1-1-onto→ 𝑇 )