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 simpr 
 |-  ( ( ph /\ g e. T ) -> g e. T )
44 breq1 
 |-  ( x = g -> ( x finSupp W <-> g finSupp W ) )
45 44 2 elrab2 
 |-  ( g e. T <-> ( g e. ( D ^m C ) /\ g finSupp W ) )
46 43 45 sylib 
 |-  ( ( ph /\ g e. T ) -> ( g e. ( D ^m C ) /\ g finSupp W ) )
47 46 simpld 
 |-  ( ( ph /\ g e. T ) -> g e. ( D ^m C ) )
48 elmapi 
 |-  ( g e. ( D ^m C ) -> g : C --> D )
49 47 48 syl 
 |-  ( ( ph /\ g e. T ) -> g : C --> D )
50 42 49 fcod 
 |-  ( ( ph /\ g e. T ) -> ( `' G o. g ) : C --> B )
51 50 adantrl 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( `' G o. g ) : C --> B )
52 fcoi1 
 |-  ( ( `' G o. g ) : C --> B -> ( ( `' G o. g ) o. ( _I |` C ) ) = ( `' G o. g ) )
53 51 52 syl 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( `' G o. g ) o. ( _I |` C ) ) = ( `' G o. g ) )
54 38 53 eqtrd 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( `' G o. g ) o. ( `' F o. F ) ) = ( `' G o. g ) )
55 34 54 eqtrid 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( ( `' G o. g ) o. `' F ) o. F ) = ( `' G o. g ) )
56 55 eqeq2d 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( f o. F ) = ( ( ( `' G o. g ) o. `' F ) o. F ) <-> ( f o. F ) = ( `' G o. g ) ) )
57 coass 
 |-  ( ( `' G o. G ) o. ( f o. F ) ) = ( `' G o. ( G o. ( f o. F ) ) )
58 5 adantr 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> G : B -1-1-onto-> D )
59 f1ococnv1 
 |-  ( G : B -1-1-onto-> D -> ( `' G o. G ) = ( _I |` B ) )
60 58 59 syl 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( `' G o. G ) = ( _I |` B ) )
61 60 coeq1d 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( `' G o. G ) o. ( f o. F ) ) = ( ( _I |` B ) o. ( f o. F ) ) )
62 24 adantrr 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( f o. F ) : C --> B )
63 fcoi2 
 |-  ( ( f o. F ) : C --> B -> ( ( _I |` B ) o. ( f o. F ) ) = ( f o. F ) )
64 62 63 syl 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( _I |` B ) o. ( f o. F ) ) = ( f o. F ) )
65 61 64 eqtrd 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( `' G o. G ) o. ( f o. F ) ) = ( f o. F ) )
66 57 65 eqtr3id 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( `' G o. ( G o. ( f o. F ) ) ) = ( f o. F ) )
67 66 eqeq2d 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( `' G o. g ) = ( `' G o. ( G o. ( f o. F ) ) ) <-> ( `' G o. g ) = ( f o. F ) ) )
68 eqcom 
 |-  ( ( `' G o. g ) = ( f o. F ) <-> ( f o. F ) = ( `' G o. g ) )
69 67 68 bitrdi 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( `' G o. g ) = ( `' G o. ( G o. ( f o. F ) ) ) <-> ( f o. F ) = ( `' G o. g ) ) )
70 56 69 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 ) ) ) ) )
71 f1ofo 
 |-  ( F : C -1-1-onto-> A -> F : C -onto-> A )
72 35 71 syl 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> F : C -onto-> A )
73 ffn 
 |-  ( f : A --> B -> f Fn A )
74 18 19 73 3syl 
 |-  ( ( ph /\ f e. S ) -> f Fn A )
75 74 adantrr 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> f Fn A )
76 f1ocnv 
 |-  ( F : C -1-1-onto-> A -> `' F : A -1-1-onto-> C )
77 f1of 
 |-  ( `' F : A -1-1-onto-> C -> `' F : A --> C )
78 4 76 77 3syl 
 |-  ( ph -> `' F : A --> C )
79 78 adantr 
 |-  ( ( ph /\ g e. T ) -> `' F : A --> C )
80 50 79 fcod 
 |-  ( ( ph /\ g e. T ) -> ( ( `' G o. g ) o. `' F ) : A --> B )
81 80 ffnd 
 |-  ( ( ph /\ g e. T ) -> ( ( `' G o. g ) o. `' F ) Fn A )
82 81 adantrl 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( `' G o. g ) o. `' F ) Fn A )
83 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 ) ) )
84 72 75 82 83 syl3anc 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( f o. F ) = ( ( ( `' G o. g ) o. `' F ) o. F ) <-> f = ( ( `' G o. g ) o. `' F ) ) )
85 5 39 syl 
 |-  ( ph -> `' G : D -1-1-onto-> B )
86 85 adantr 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> `' G : D -1-1-onto-> B )
87 f1of1 
 |-  ( `' G : D -1-1-onto-> B -> `' G : D -1-1-> B )
88 86 87 syl 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> `' G : D -1-1-> B )
89 49 adantrl 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> g : C --> D )
90 25 adantrr 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( G o. ( f o. F ) ) : C --> D )
91 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 ) ) ) )
92 88 89 90 91 syl3anc 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( ( `' G o. g ) = ( `' G o. ( G o. ( f o. F ) ) ) <-> g = ( G o. ( f o. F ) ) ) )
93 70 84 92 3bitr3d 
 |-  ( ( ph /\ ( f e. S /\ g e. T ) ) -> ( f = ( ( `' G o. g ) o. `' F ) <-> g = ( G o. ( f o. F ) ) ) )
94 11 32 33 93 f1o2d 
 |-  ( ph -> ( f e. S |-> ( G o. ( f o. F ) ) ) : S -1-1-onto-> T )