Metamath Proof Explorer

Theorem mapfienlem1

Description: Lemma 1 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 mapfienlem1 
|- ( ( ph /\ f e. S ) -> ( G o. ( f o. F ) ) finSupp W )

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 3 fvexi 
 |-  W e. _V
12 11 a1i 
 |-  ( ( ph /\ f e. S ) -> W e. _V )
13 10 adantr 
 |-  ( ( ph /\ f e. S ) -> Z e. B )
14 elrabi 
 |-  ( f e. { x e. ( B ^m A ) | x finSupp Z } -> f e. ( B ^m A ) )
15 elmapi 
 |-  ( f e. ( B ^m A ) -> f : A --> B )
16 14 15 syl 
 |-  ( f e. { x e. ( B ^m A ) | x finSupp Z } -> f : A --> B )
17 16 1 eleq2s 
 |-  ( f e. S -> f : A --> B )
18 f1of 
 |-  ( F : C -1-1-onto-> A -> F : C --> A )
19 4 18 syl 
 |-  ( ph -> F : C --> A )
20 fco 
 |-  ( ( f : A --> B /\ F : C --> A ) -> ( f o. F ) : C --> B )
21 17 19 20 syl2anr 
 |-  ( ( ph /\ f e. S ) -> ( f o. F ) : C --> B )
22 f1of 
 |-  ( G : B -1-1-onto-> D -> G : B --> D )
23 5 22 syl 
 |-  ( ph -> G : B --> D )
24 23 adantr 
 |-  ( ( ph /\ f e. S ) -> G : B --> D )
25 ssidd 
 |-  ( ( ph /\ f e. S ) -> B C_ B )
26 8 adantr 
 |-  ( ( ph /\ f e. S ) -> C e. X )
27 7 adantr 
 |-  ( ( ph /\ f e. S ) -> B e. V )
28 breq1 
 |-  ( x = f -> ( x finSupp Z <-> f finSupp Z ) )
29 28 1 elrab2 
 |-  ( f e. S <-> ( f e. ( B ^m A ) /\ f finSupp Z ) )
30 29 simprbi 
 |-  ( f e. S -> f finSupp Z )
31 30 adantl 
 |-  ( ( ph /\ f e. S ) -> f finSupp Z )
32 f1of1 
 |-  ( F : C -1-1-onto-> A -> F : C -1-1-> A )
33 4 32 syl 
 |-  ( ph -> F : C -1-1-> A )
34 33 adantr 
 |-  ( ( ph /\ f e. S ) -> F : C -1-1-> A )
35 simpr 
 |-  ( ( ph /\ f e. S ) -> f e. S )
36 31 34 13 35 fsuppco 
 |-  ( ( ph /\ f e. S ) -> ( f o. F ) finSupp Z )
37 3 eqcomi 
 |-  ( G ` Z ) = W
38 37 a1i 
 |-  ( ( ph /\ f e. S ) -> ( G ` Z ) = W )
39 12 13 21 24 25 26 27 36 38 fsuppcor 
 |-  ( ( ph /\ f e. S ) -> ( G o. ( f o. F ) ) finSupp W )