Metamath Proof Explorer

Theorem fcobijfs2

Description: Composing finitely supported functions with a bijection yields a bijection between sets of finitely supported functions. See also fcobijfs and mapfien . (Contributed by Thierry Arnoux, 10-Jan-2026)

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

Proof

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