Metamath Proof Explorer

Theorem fcobijfs

Description: Composing finitely supported functions with a bijection yields a bijection between sets of finitely supported functions. See also mapfien . (Contributed by Thierry Arnoux, 25-Aug-2017) (Revised by Thierry Arnoux, 1-Sep-2019)

Ref Expression
Hypotheses fcobij.1 
|- ( ph -> G : S -1-1-onto-> T )
fcobij.2 
|- ( ph -> R e. U )
fcobij.3 
|- ( ph -> S e. V )
fcobij.4 
|- ( ph -> T e. W )
fcobijfs.5 
|- ( ph -> O e. S )
fcobijfs.6 
|- Q = ( G ` O )
fcobijfs.7 
|- X = { g e. ( S ^m R ) | g finSupp O }
fcobijfs.8 
|- Y = { h e. ( T ^m R ) | h finSupp Q }
Assertion fcobijfs 
|- ( ph -> ( f e. X |-> ( G o. f ) ) : X -1-1-onto-> Y )

Proof

Step Hyp Ref Expression
1 fcobij.1 
 |-  ( ph -> G : S -1-1-onto-> T )
2 fcobij.2 
 |-  ( ph -> R e. U )
3 fcobij.3 
 |-  ( ph -> S e. V )
4 fcobij.4 
 |-  ( ph -> T e. W )
5 fcobijfs.5 
 |-  ( ph -> O e. S )
6 fcobijfs.6 
 |-  Q = ( G ` O )
7 fcobijfs.7 
 |-  X = { g e. ( S ^m R ) | g finSupp O }
8 fcobijfs.8 
 |-  Y = { h e. ( T ^m R ) | h finSupp Q }
9 breq1 
 |-  ( h = g -> ( h finSupp O <-> g finSupp O ) )
10 9 cbvrabv 
 |-  { h e. ( S ^m R ) | h finSupp O } = { g e. ( S ^m R ) | g finSupp O }
11 7 10 eqtr4i 
 |-  X = { h e. ( S ^m R ) | h finSupp O }
12 f1oi 
 |-  ( _I |` R ) : R -1-1-onto-> R
13 12 a1i 
 |-  ( ph -> ( _I |` R ) : R -1-1-onto-> R )
14 11 8 6 13 1 2 3 2 4 5 mapfien 
 |-  ( ph -> ( f e. X |-> ( G o. ( f o. ( _I |` R ) ) ) ) : X -1-1-onto-> Y )
15 7 ssrab3 
 |-  X C_ ( S ^m R )
16 15 sseli 
 |-  ( f e. X -> f e. ( S ^m R ) )
17 coass 
 |-  ( ( G o. f ) o. ( _I |` R ) ) = ( G o. ( f o. ( _I |` R ) ) )
18 f1of 
 |-  ( G : S -1-1-onto-> T -> G : S --> T )
19 1 18 syl 
 |-  ( ph -> G : S --> T )
20 elmapi 
 |-  ( f e. ( S ^m R ) -> f : R --> S )
21 fco 
 |-  ( ( G : S --> T /\ f : R --> S ) -> ( G o. f ) : R --> T )
22 19 20 21 syl2an 
 |-  ( ( ph /\ f e. ( S ^m R ) ) -> ( G o. f ) : R --> T )
23 fcoi1 
 |-  ( ( G o. f ) : R --> T -> ( ( G o. f ) o. ( _I |` R ) ) = ( G o. f ) )
24 22 23 syl 
 |-  ( ( ph /\ f e. ( S ^m R ) ) -> ( ( G o. f ) o. ( _I |` R ) ) = ( G o. f ) )
25 17 24 eqtr3id 
 |-  ( ( ph /\ f e. ( S ^m R ) ) -> ( G o. ( f o. ( _I |` R ) ) ) = ( G o. f ) )
26 16 25 sylan2 
 |-  ( ( ph /\ f e. X ) -> ( G o. ( f o. ( _I |` R ) ) ) = ( G o. f ) )
27 26 mpteq2dva 
 |-  ( ph -> ( f e. X |-> ( G o. ( f o. ( _I |` R ) ) ) ) = ( f e. X |-> ( G o. f ) ) )
28 27 f1oeq1d 
 |-  ( ph -> ( ( f e. X |-> ( G o. ( f o. ( _I |` R ) ) ) ) : X -1-1-onto-> Y <-> ( f e. X |-> ( G o. f ) ) : X -1-1-onto-> Y ) )
29 14 28 mpbid 
 |-  ( ph -> ( f e. X |-> ( G o. f ) ) : X -1-1-onto-> Y )