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 )