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		f1oeq1	|- ( ( f e. X |-> ( G o. ( f o. ( _I |` R ) ) ) ) = ( f e. X |-> ( G o. f ) ) -> ( ( 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	27 28	syl	|- ( 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 ) )
30	14 29	mpbid	|- ( ph -> ( f e. X |-> ( G o. f ) ) : X -1-1-onto-> Y )