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 breq1 ⊢ ( 𝑥 = 𝑔 → ( 𝑥 finSupp 𝑊 ↔ 𝑔 finSupp 𝑊 ) )
44 43 2 elrab2 ⊢ ( 𝑔 ∈ 𝑇 ↔ ( 𝑔 ∈ ( 𝐷 ↑m 𝐶 ) ∧ 𝑔 finSupp 𝑊 ) )
45 44 bilani ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ( 𝑔 ∈ ( 𝐷 ↑m 𝐶 ) ∧ 𝑔 finSupp 𝑊 ) )
46 45 simpld ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → 𝑔 ∈ ( 𝐷 ↑m 𝐶 ) )
47 elmapi ⊢ ( 𝑔 ∈ ( 𝐷 ↑m 𝐶 ) → 𝑔 : 𝐶 ⟶ 𝐷 )
48 46 47 syl ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → 𝑔 : 𝐶 ⟶ 𝐷 )
49 42 48 fcod ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ( ◡ 𝐺 ∘ 𝑔 ) : 𝐶 ⟶ 𝐵 )
50 49 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ◡ 𝐺 ∘ 𝑔 ) : 𝐶 ⟶ 𝐵 )
51 fcoi1 ⊢ ( ( ◡ 𝐺 ∘ 𝑔 ) : 𝐶 ⟶ 𝐵 → ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ( I ↾ 𝐶 ) ) = ( ◡ 𝐺 ∘ 𝑔 ) )
52 50 51 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ( I ↾ 𝐶 ) ) = ( ◡ 𝐺 ∘ 𝑔 ) )
53 38 52 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ( ◡ 𝐹 ∘ 𝐹 ) ) = ( ◡ 𝐺 ∘ 𝑔 ) )
54 34 53 eqtrid ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ∘ 𝐹 ) = ( ◡ 𝐺 ∘ 𝑔 ) )
55 54 eqeq2d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( 𝑓 ∘ 𝐹 ) = ( ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ∘ 𝐹 ) ↔ ( 𝑓 ∘ 𝐹 ) = ( ◡ 𝐺 ∘ 𝑔 ) ) )
56 coass ⊢ ( ( ◡ 𝐺 ∘ 𝐺 ) ∘ ( 𝑓 ∘ 𝐹 ) ) = ( ◡ 𝐺 ∘ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) )
57 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → 𝐺 : 𝐵 –1-1-onto→ 𝐷 )
58 f1ococnv1 ⊢ ( 𝐺 : 𝐵 –1-1-onto→ 𝐷 → ( ◡ 𝐺 ∘ 𝐺 ) = ( I ↾ 𝐵 ) )
59 57 58 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ◡ 𝐺 ∘ 𝐺 ) = ( I ↾ 𝐵 ) )
60 59 coeq1d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( ◡ 𝐺 ∘ 𝐺 ) ∘ ( 𝑓 ∘ 𝐹 ) ) = ( ( I ↾ 𝐵 ) ∘ ( 𝑓 ∘ 𝐹 ) ) )
61 24 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( 𝑓 ∘ 𝐹 ) : 𝐶 ⟶ 𝐵 )
62 fcoi2 ⊢ ( ( 𝑓 ∘ 𝐹 ) : 𝐶 ⟶ 𝐵 → ( ( I ↾ 𝐵 ) ∘ ( 𝑓 ∘ 𝐹 ) ) = ( 𝑓 ∘ 𝐹 ) )
63 61 62 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( I ↾ 𝐵 ) ∘ ( 𝑓 ∘ 𝐹 ) ) = ( 𝑓 ∘ 𝐹 ) )
64 60 63 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( ◡ 𝐺 ∘ 𝐺 ) ∘ ( 𝑓 ∘ 𝐹 ) ) = ( 𝑓 ∘ 𝐹 ) )
65 56 64 eqtr3id ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ◡ 𝐺 ∘ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) = ( 𝑓 ∘ 𝐹 ) )
66 65 eqeq2d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( ◡ 𝐺 ∘ 𝑔 ) = ( ◡ 𝐺 ∘ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ↔ ( ◡ 𝐺 ∘ 𝑔 ) = ( 𝑓 ∘ 𝐹 ) ) )
67 eqcom ⊢ ( ( ◡ 𝐺 ∘ 𝑔 ) = ( 𝑓 ∘ 𝐹 ) ↔ ( 𝑓 ∘ 𝐹 ) = ( ◡ 𝐺 ∘ 𝑔 ) )
68 66 67 bitrdi ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( ◡ 𝐺 ∘ 𝑔 ) = ( ◡ 𝐺 ∘ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ↔ ( 𝑓 ∘ 𝐹 ) = ( ◡ 𝐺 ∘ 𝑔 ) ) )
69 55 68 bitr4d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( 𝑓 ∘ 𝐹 ) = ( ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ∘ 𝐹 ) ↔ ( ◡ 𝐺 ∘ 𝑔 ) = ( ◡ 𝐺 ∘ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ) )
70 f1ofo ⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝐴 → 𝐹 : 𝐶 –onto→ 𝐴 )
71 35 70 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → 𝐹 : 𝐶 –onto→ 𝐴 )
72 ffn ⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 → 𝑓 Fn 𝐴 )
73 18 19 72 3syl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑆 ) → 𝑓 Fn 𝐴 )
74 73 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → 𝑓 Fn 𝐴 )
75 f1ocnv ⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝐴 → ◡ 𝐹 : 𝐴 –1-1-onto→ 𝐶 )
76 f1of ⊢ ( ◡ 𝐹 : 𝐴 –1-1-onto→ 𝐶 → ◡ 𝐹 : 𝐴 ⟶ 𝐶 )
77 4 75 76 3syl ⊢ ( 𝜑 → ◡ 𝐹 : 𝐴 ⟶ 𝐶 )
78 77 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ◡ 𝐹 : 𝐴 ⟶ 𝐶 )
79 49 78 fcod ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) : 𝐴 ⟶ 𝐵 )
80 79 ffnd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) Fn 𝐴 )
81 80 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) Fn 𝐴 )
82 cocan2 ⊢ ( ( 𝐹 : 𝐶 –onto→ 𝐴 ∧ 𝑓 Fn 𝐴 ∧ ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) Fn 𝐴 ) → ( ( 𝑓 ∘ 𝐹 ) = ( ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ∘ 𝐹 ) ↔ 𝑓 = ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ) )
83 71 74 81 82 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( 𝑓 ∘ 𝐹 ) = ( ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ∘ 𝐹 ) ↔ 𝑓 = ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ) )
84 5 39 syl ⊢ ( 𝜑 → ◡ 𝐺 : 𝐷 –1-1-onto→ 𝐵 )
85 84 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ◡ 𝐺 : 𝐷 –1-1-onto→ 𝐵 )
86 f1of1 ⊢ ( ◡ 𝐺 : 𝐷 –1-1-onto→ 𝐵 → ◡ 𝐺 : 𝐷 –1-1→ 𝐵 )
87 85 86 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ◡ 𝐺 : 𝐷 –1-1→ 𝐵 )
88 48 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → 𝑔 : 𝐶 ⟶ 𝐷 )
89 25 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) : 𝐶 ⟶ 𝐷 )
90 cocan1 ⊢ ( ( ◡ 𝐺 : 𝐷 –1-1→ 𝐵 ∧ 𝑔 : 𝐶 ⟶ 𝐷 ∧ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) : 𝐶 ⟶ 𝐷 ) → ( ( ◡ 𝐺 ∘ 𝑔 ) = ( ◡ 𝐺 ∘ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ↔ 𝑔 = ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) )
91 87 88 89 90 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( ( ◡ 𝐺 ∘ 𝑔 ) = ( ◡ 𝐺 ∘ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) ↔ 𝑔 = ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) )
92 69 83 91 3bitr3d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑇 ) ) → ( 𝑓 = ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) ↔ 𝑔 = ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) )
93 11 32 33 92 f1o2d ⊢ ( 𝜑 → ( 𝑓 ∈ 𝑆 ↦ ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) ) : 𝑆 –1-1-onto→ 𝑇 )