This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mapfienlem3

Description: Lemma 3 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 mapfienlem3 
|- ( ( ph /\ g e. T ) -> ( ( `' G o. g ) o. `' F ) e. S )

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 f1ocnv 
 |-  ( G : B -1-1-onto-> D -> `' G : D -1-1-onto-> B )
12 f1of 
 |-  ( `' G : D -1-1-onto-> B -> `' G : D --> B )
13 5 11 12 3syl 
 |-  ( ph -> `' G : D --> B )
14 13 adantr 
 |-  ( ( ph /\ g e. T ) -> `' G : D --> B )
15 elrabi 
 |-  ( g e. { x e. ( D ^m C ) | x finSupp W } -> g e. ( D ^m C ) )
16 15 2 eleq2s 
 |-  ( g e. T -> g e. ( D ^m C ) )
17 16 adantl 
 |-  ( ( ph /\ g e. T ) -> g e. ( D ^m C ) )
18 elmapi 
 |-  ( g e. ( D ^m C ) -> g : C --> D )
19 17 18 syl 
 |-  ( ( ph /\ g e. T ) -> g : C --> D )
20 14 19 fcod 
 |-  ( ( ph /\ g e. T ) -> ( `' G o. g ) : C --> B )
21 f1ocnv 
 |-  ( F : C -1-1-onto-> A -> `' F : A -1-1-onto-> C )
22 f1of 
 |-  ( `' F : A -1-1-onto-> C -> `' F : A --> C )
23 4 21 22 3syl 
 |-  ( ph -> `' F : A --> C )
24 23 adantr 
 |-  ( ( ph /\ g e. T ) -> `' F : A --> C )
25 20 24 fcod 
 |-  ( ( ph /\ g e. T ) -> ( ( `' G o. g ) o. `' F ) : A --> B )
26 7 6 elmapd 
 |-  ( ph -> ( ( ( `' G o. g ) o. `' F ) e. ( B ^m A ) <-> ( ( `' G o. g ) o. `' F ) : A --> B ) )
27 26 adantr 
 |-  ( ( ph /\ g e. T ) -> ( ( ( `' G o. g ) o. `' F ) e. ( B ^m A ) <-> ( ( `' G o. g ) o. `' F ) : A --> B ) )
28 25 27 mpbird 
 |-  ( ( ph /\ g e. T ) -> ( ( `' G o. g ) o. `' F ) e. ( B ^m A ) )
29 1 2 3 4 5 6 7 8 9 10 mapfienlem2 
 |-  ( ( ph /\ g e. T ) -> ( ( `' G o. g ) o. `' F ) finSupp Z )
30 breq1 
 |-  ( x = ( ( `' G o. g ) o. `' F ) -> ( x finSupp Z <-> ( ( `' G o. g ) o. `' F ) finSupp Z ) )
31 30 1 elrab2 
 |-  ( ( ( `' G o. g ) o. `' F ) e. S <-> ( ( ( `' G o. g ) o. `' F ) e. ( B ^m A ) /\ ( ( `' G o. g ) o. `' F ) finSupp Z ) )
32 28 29 31 sylanbrc 
 |-  ( ( ph /\ g e. T ) -> ( ( `' G o. g ) o. `' F ) e. S )