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 
|- S = { x e. ( B ^m A ) | x finSupp Z }
mapfien.t 
|- T = { x e. ( D ^m C ) | x finSupp W }
mapfien.w 
|- W = ( G ` Z )
mapfien.f 
|- ( ph -> F : C -1-1-onto-> A )
mapfien.g 
|- ( ph -> G : B -1-1-onto-> D )
mapfien.a 
|- ( ph -> A e. U )
mapfien.b 
|- ( ph -> B e. V )
mapfien.c 
|- ( ph -> C e. X )
mapfien.d 
|- ( ph -> D e. Y )
mapfien.z 
|- ( ph -> Z e. B )
Assertion mapfien 
|- ( ph -> ( f e. S |-> ( G o. ( f o. F ) ) ) : S -1-1-onto-> T )

Proof

Step Hyp Ref Expression
1 mapfien.s 
 |-  S = { x e. ( B ^m A ) | x finSupp Z }
2 mapfien.t 
 |-  T = { x e. ( D ^m C ) | x finSupp W }
3 mapfien.w 
 |-  W = ( G ` Z )
4 mapfien.f 
 |-  ( ph -> F : C -1-1-onto-> A )
5 mapfien.g 
 |-  ( ph -> G : B -1-1-onto-> D )
6 mapfien.a 
 |-  ( ph -> A e. U )
7 mapfien.b 
 |-  ( ph -> B e. V )
8 mapfien.c 
 |-  ( ph -> C e. X )
9 mapfien.d 
 |-  ( ph -> D e. Y )
10 mapfien.z 
 |-  ( ph -> Z e. B )
11 eqid 
 |-  ( f e. S |-> ( G o. ( f o. F ) ) ) = ( f e. S |-> ( G o. ( f o. F ) ) )
12 f1of 
 |-  ( G : B -1-1-onto-> D -> G : B --> D )
13 5 12 syl 
 |-  ( ph -> G : B --> D )
14 13 adantr 
 |-  ( ( ph /\ f e. S ) -> G : B --> D )
15 breq1 
 |-  ( x = f -> ( x finSupp Z <-> f finSupp Z ) )
16 15 1 elrab2 
 |-  ( f e. S <-> ( f e. ( B ^m A ) /\ f finSupp Z ) )
17 16 simplbi 
 |-  ( f e. S -> f e. ( B ^m A ) )
18 17 adantl 
 |-  ( ( ph /\ f e. S ) -> f e. ( B ^m A ) )
19 elmapi 
 |-  ( f e. ( B ^m A ) -> f : A --> B )
20 18 19 syl 
 |-  ( ( ph /\ f e. S ) -> f : A --> B )
21 f1of 
 |-  ( F : C -1-1-onto-> A -> F : C --> A )
22 4 21 syl 
 |-  ( ph -> F : C --> A )
23 22 adantr 
 |-  ( ( ph /\ f e. S ) -> F : C --> A )
24 20 23 fcod 
 |-  ( ( ph /\ f e. S ) -> ( f o. F ) : C --> B )
25 14 24 fcod 
 |-  ( ( ph /\ f e. S ) -> ( G o. ( f o. F ) ) : C --> D )
26 9 8 elmapd 
 |-  ( ph -> ( ( G o. ( f o. F ) ) e. ( D ^m C ) <-> ( G o. ( f o. F ) ) : C --> D ) )
27 26 adantr 
 |-  ( ( ph /\ f e. S ) -> ( ( G o. ( f o. F ) ) e. ( D ^m C ) <-> ( G o. ( f o. F ) ) : C --> D ) )
28 25 27 mpbird 
 |-  ( ( ph /\ f e. S ) -> ( G o. ( f o. F ) ) e. ( D ^m C ) )
29 1 2 3 4 5 6 7 8 9 10 mapfienlem1 
 |-  ( ( ph /\ f e. S ) -> ( G o. ( f o. F ) ) finSupp W )
30 breq1 
 |-  ( x = ( G o. ( f o. F ) ) -> ( x finSupp W <-> ( G o. ( f o. F ) ) finSupp W ) )
31 30 2 elrab2 
 |-  ( ( G o. ( f o. F ) ) e. T <-> ( ( G o. ( f o. F ) ) e. ( D ^m C ) /\ ( G o. ( f o. F ) ) finSupp W ) )
32 28 29 31 sylanbrc 
 |-  ( ( ph /\ f e. S ) -> ( G o. ( f o. F ) ) e. T )
33 1 2 3 4 5 6 7 8 9 10 mapfienlem3 
 |-  ( ( ph /\ g e. T ) -> ( ( `' G o. g ) o. `' F ) e. S )
34 coass 
 |-  ( ( ( `' G o. g ) o. `' F ) o. F ) = ( ( `' G o. g ) o. ( `' F o. F ) )
35 4 adantr 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> F : C -1-1-onto-> A )
36 f1ococnv1 
 |-  ( F : C -1-1-onto-> A -> ( `' F o. F ) = ( _I |` C ) )
37 35 36 syl 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( `' F o. F ) = ( _I |` C ) )
38 37 coeq2d 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( `' G o. g ) o. ( `' F o. F ) ) = ( ( `' G o. g ) o. ( _I |` C ) ) )
39 f1ocnv 
 |-  ( G : B -1-1-onto-> D -> `' G : D -1-1-onto-> B )
40 f1of 
 |-  ( `' G : D -1-1-onto-> B -> `' G : D --> B )
41 5 39 40 3syl 
 |-  ( ph -> `' G : D --> B )
42 41 adantr 
 |-  ( ( ph /\ g e. T ) -> `' G : D --> B )
43 breq1 
 |-  ( x = g -> ( x finSupp W <-> g finSupp W ) )
44 43 2 elrab2 
 |-  ( g e. T <-> ( g e. ( D ^m C ) /\ g finSupp W ) )
45 44 bilani 
 |-  ( ( ph /\ g e. T ) -> ( g e. ( D ^m C ) /\ g finSupp W ) )
46 45 simpld 
 |-  ( ( ph /\ g e. T ) -> g e. ( D ^m C ) )
47 elmapi 
 |-  ( g e. ( D ^m C ) -> g : C --> D )
48 46 47 syl 
 |-  ( ( ph /\ g e. T ) -> g : C --> D )
49 42 48 fcod 
 |-  ( ( ph /\ g e. T ) -> ( `' G o. g ) : C --> B )
50 49 adantrl 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( `' G o. g ) : C --> B )
51 fcoi1 
 |-  ( ( `' G o. g ) : C --> B -> ( ( `' G o. g ) o. ( _I |` C ) ) = ( `' G o. g ) )
52 50 51 syl 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( `' G o. g ) o. ( _I |` C ) ) = ( `' G o. g ) )
53 38 52 eqtrd 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( `' G o. g ) o. ( `' F o. F ) ) = ( `' G o. g ) )
54 34 53 eqtrid 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( ( `' G o. g ) o. `' F ) o. F ) = ( `' G o. g ) )
55 54 eqeq2d 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( f o. F ) = ( ( ( `' G o. g ) o. `' F ) o. F ) <-> ( f o. F ) = ( `' G o. g ) ) )
56 coass 
 |-  ( ( `' G o. G ) o. ( f o. F ) ) = ( `' G o. ( G o. ( f o. F ) ) )
57 5 adantr 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> G : B -1-1-onto-> D )
58 f1ococnv1 
 |-  ( G : B -1-1-onto-> D -> ( `' G o. G ) = ( _I |` B ) )
59 57 58 syl 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( `' G o. G ) = ( _I |` B ) )
60 59 coeq1d 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( `' G o. G ) o. ( f o. F ) ) = ( ( _I |` B ) o. ( f o. F ) ) )
61 24 adantrr 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( f o. F ) : C --> B )
62 fcoi2 
 |-  ( ( f o. F ) : C --> B -> ( ( _I |` B ) o. ( f o. F ) ) = ( f o. F ) )
63 61 62 syl 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( _I |` B ) o. ( f o. F ) ) = ( f o. F ) )
64 60 63 eqtrd 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( `' G o. G ) o. ( f o. F ) ) = ( f o. F ) )
65 56 64 eqtr3id 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( `' G o. ( G o. ( f o. F ) ) ) = ( f o. F ) )
66 65 eqeq2d 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( `' G o. g ) = ( `' G o. ( G o. ( f o. F ) ) ) <-> ( `' G o. g ) = ( f o. F ) ) )
67 eqcom 
 |-  ( ( `' G o. g ) = ( f o. F ) <-> ( f o. F ) = ( `' G o. g ) )
68 66 67 bitrdi 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( `' G o. g ) = ( `' G o. ( G o. ( f o. F ) ) ) <-> ( f o. F ) = ( `' G o. g ) ) )
69 55 68 bitr4d 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( f o. F ) = ( ( ( `' G o. g ) o. `' F ) o. F ) <-> ( `' G o. g ) = ( `' G o. ( G o. ( f o. F ) ) ) ) )
70 f1ofo 
 |-  ( F : C -1-1-onto-> A -> F : C -onto-> A )
71 35 70 syl 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> F : C -onto-> A )
72 ffn 
 |-  ( f : A --> B -> f Fn A )
73 18 19 72 3syl 
 |-  ( ( ph /\ f e. S ) -> f Fn A )
74 73 adantrr 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> f Fn A )
75 f1ocnv 
 |-  ( F : C -1-1-onto-> A -> `' F : A -1-1-onto-> C )
76 f1of 
 |-  ( `' F : A -1-1-onto-> C -> `' F : A --> C )
77 4 75 76 3syl 
 |-  ( ph -> `' F : A --> C )
78 77 adantr 
 |-  ( ( ph /\ g e. T ) -> `' F : A --> C )
79 49 78 fcod 
 |-  ( ( ph /\ g e. T ) -> ( ( `' G o. g ) o. `' F ) : A --> B )
80 79 ffnd 
 |-  ( ( ph /\ g e. T ) -> ( ( `' G o. g ) o. `' F ) Fn A )
81 80 adantrl 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( `' G o. g ) o. `' F ) Fn A )
82 cocan2 
 |-  ( ( F : C -onto-> A /\ f Fn A /\ ( ( `' G o. g ) o. `' F ) Fn A ) -> ( ( f o. F ) = ( ( ( `' G o. g ) o. `' F ) o. F ) <-> f = ( ( `' G o. g ) o. `' F ) ) )
83 71 74 81 82 syl3anc 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( f o. F ) = ( ( ( `' G o. g ) o. `' F ) o. F ) <-> f = ( ( `' G o. g ) o. `' F ) ) )
84 5 39 syl 
 |-  ( ph -> `' G : D -1-1-onto-> B )
85 84 adantr 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> `' G : D -1-1-onto-> B )
86 f1of1 
 |-  ( `' G : D -1-1-onto-> B -> `' G : D -1-1-> B )
87 85 86 syl 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> `' G : D -1-1-> B )
88 48 adantrl 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> g : C --> D )
89 25 adantrr 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( G o. ( f o. F ) ) : C --> D )
90 cocan1 
 |-  ( ( `' G : D -1-1-> B /\ g : C --> D /\ ( G o. ( f o. F ) ) : C --> D ) -> ( ( `' G o. g ) = ( `' G o. ( G o. ( f o. F ) ) ) <-> g = ( G o. ( f o. F ) ) ) )
91 87 88 89 90 syl3anc 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( `' G o. g ) = ( `' G o. ( G o. ( f o. F ) ) ) <-> g = ( G o. ( f o. F ) ) ) )
92 69 83 91 3bitr3d 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( f = ( ( `' G o. g ) o. `' F ) <-> g = ( G o. ( f o. F ) ) ) )
93 11 32 33 92 f1o2d 
 |-  ( ph -> ( f e. S |-> ( G o. ( f o. F ) ) ) : S -1-1-onto-> T )