Metamath Proof Explorer

Theorem mapfienlem2

Description: Lemma 2 for mapfien . (Contributed 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 mapfienlem2 
|- ( ( ph /\ g e. T ) -> ( ( `' G o. g ) o. `' F ) finSupp Z )

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 10 adantr 
 |-  ( ( ph /\ g e. T ) -> Z e. B )
12 f1of 
 |-  ( G : B -1-1-onto-> D -> G : B --> D )
13 5 12 syl 
 |-  ( ph -> G : B --> D )
14 13 10 ffvelcdmd 
 |-  ( ph -> ( G ` Z ) e. D )
15 3 14 eqeltrid 
 |-  ( ph -> W e. D )
16 15 adantr 
 |-  ( ( ph /\ g e. T ) -> W e. D )
17 elrabi 
 |-  ( g e. { x e. ( D ^m C ) | x finSupp W } -> g e. ( D ^m C ) )
18 elmapi 
 |-  ( g e. ( D ^m C ) -> g : C --> D )
19 17 18 syl 
 |-  ( g e. { x e. ( D ^m C ) | x finSupp W } -> g : C --> D )
20 19 2 eleq2s 
 |-  ( g e. T -> g : C --> D )
21 20 adantl 
 |-  ( ( ph /\ g e. T ) -> g : C --> D )
22 f1ocnv 
 |-  ( G : B -1-1-onto-> D -> `' G : D -1-1-onto-> B )
23 f1of 
 |-  ( `' G : D -1-1-onto-> B -> `' G : D --> B )
24 5 22 23 3syl 
 |-  ( ph -> `' G : D --> B )
25 24 adantr 
 |-  ( ( ph /\ g e. T ) -> `' G : D --> B )
26 ssidd 
 |-  ( ( ph /\ g e. T ) -> D C_ D )
27 8 adantr 
 |-  ( ( ph /\ g e. T ) -> C e. X )
28 9 adantr 
 |-  ( ( ph /\ g e. T ) -> D e. Y )
29 breq1 
 |-  ( x = g -> ( x finSupp W <-> g finSupp W ) )
30 29 elrab 
 |-  ( g e. { x e. ( D ^m C ) | x finSupp W } <-> ( g e. ( D ^m C ) /\ g finSupp W ) )
31 30 simprbi 
 |-  ( g e. { x e. ( D ^m C ) | x finSupp W } -> g finSupp W )
32 31 2 eleq2s 
 |-  ( g e. T -> g finSupp W )
33 32 adantl 
 |-  ( ( ph /\ g e. T ) -> g finSupp W )
34 5 10 jca 
 |-  ( ph -> ( G : B -1-1-onto-> D /\ Z e. B ) )
35 3 eqcomi 
 |-  ( G ` Z ) = W
36 34 35 jctir 
 |-  ( ph -> ( ( G : B -1-1-onto-> D /\ Z e. B ) /\ ( G ` Z ) = W ) )
37 36 adantr 
 |-  ( ( ph /\ g e. T ) -> ( ( G : B -1-1-onto-> D /\ Z e. B ) /\ ( G ` Z ) = W ) )
38 f1ocnvfv 
 |-  ( ( G : B -1-1-onto-> D /\ Z e. B ) -> ( ( G ` Z ) = W -> ( `' G ` W ) = Z ) )
39 38 imp 
 |-  ( ( ( G : B -1-1-onto-> D /\ Z e. B ) /\ ( G ` Z ) = W ) -> ( `' G ` W ) = Z )
40 37 39 syl 
 |-  ( ( ph /\ g e. T ) -> ( `' G ` W ) = Z )
41 11 16 21 25 26 27 28 33 40 fsuppcor 
 |-  ( ( ph /\ g e. T ) -> ( `' G o. g ) finSupp Z )
42 f1ocnv 
 |-  ( F : C -1-1-onto-> A -> `' F : A -1-1-onto-> C )
43 f1of1 
 |-  ( `' F : A -1-1-onto-> C -> `' F : A -1-1-> C )
44 4 42 43 3syl 
 |-  ( ph -> `' F : A -1-1-> C )
45 44 adantr 
 |-  ( ( ph /\ g e. T ) -> `' F : A -1-1-> C )
46 13 7 jca 
 |-  ( ph -> ( G : B --> D /\ B e. V ) )
47 fex 
 |-  ( ( G : B --> D /\ B e. V ) -> G e. _V )
48 cnvexg 
 |-  ( G e. _V -> `' G e. _V )
49 46 47 48 3syl 
 |-  ( ph -> `' G e. _V )
50 coexg 
 |-  ( ( `' G e. _V /\ g e. T ) -> ( `' G o. g ) e. _V )
51 49 50 sylan 
 |-  ( ( ph /\ g e. T ) -> ( `' G o. g ) e. _V )
52 41 45 11 51 fsuppco 
 |-  ( ( ph /\ g e. T ) -> ( ( `' G o. g ) o. `' F ) finSupp Z )