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𝑇 )