Theorem fsuppco

Description: The composition of a 1-1 function with a finitely supported function is finitely supported. (Contributed by AV, 28-May-2019)

	Ref	Expression
Hypotheses	fsuppco.f	|- ( ph -> F finSupp Z )
	fsuppco.g	|- ( ph -> G : X -1-1-> Y )
	fsuppco.z	|- ( ph -> Z e. W )
	fsuppco.v	|- ( ph -> F e. V )
Assertion	fsuppco	|- ( ph -> ( F o. G ) finSupp Z )

Proof

Step	Hyp	Ref	Expression
1		fsuppco.f	|- ( ph -> F finSupp Z )
2		fsuppco.g	|- ( ph -> G : X -1-1-> Y )
3		fsuppco.z	|- ( ph -> Z e. W )
4		fsuppco.v	|- ( ph -> F e. V )
5		df-f1	|- ( G : X -1-1-> Y <-> ( G : X --> Y /\ Fun `' G ) )
6	5	simprbi	|- ( G : X -1-1-> Y -> Fun `' G )
7	2 6	syl	|- ( ph -> Fun `' G )
8		cofunex2g	|- ( ( F e. V /\ Fun `' G ) -> ( F o. G ) e. _V )
9	4 7 8	syl2anc	|- ( ph -> ( F o. G ) e. _V )
10		suppimacnv	|- ( ( ( F o. G ) e. _V /\ Z e. W ) -> ( ( F o. G ) supp Z ) = ( `' ( F o. G ) " ( _V \ { Z } ) ) )
11	9 3 10	syl2anc	|- ( ph -> ( ( F o. G ) supp Z ) = ( `' ( F o. G ) " ( _V \ { Z } ) ) )
12		suppimacnv	|- ( ( F e. V /\ Z e. W ) -> ( F supp Z ) = ( `' F " ( _V \ { Z } ) ) )
13	4 3 12	syl2anc	|- ( ph -> ( F supp Z ) = ( `' F " ( _V \ { Z } ) ) )
14	1	fsuppimpd	|- ( ph -> ( F supp Z ) e. Fin )
15	13 14	eqeltrrd	|- ( ph -> ( `' F " ( _V \ { Z } ) ) e. Fin )
16	15 2	fsuppcolem	|- ( ph -> ( `' ( F o. G ) " ( _V \ { Z } ) ) e. Fin )
17	11 16	eqeltrd	|- ( ph -> ( ( F o. G ) supp Z ) e. Fin )
18		fsuppimp	|- ( F finSupp Z -> ( Fun F /\ ( F supp Z ) e. Fin ) )
19	18	simpld	|- ( F finSupp Z -> Fun F )
20	1 19	syl	|- ( ph -> Fun F )
21		f1fun	|- ( G : X -1-1-> Y -> Fun G )
22	2 21	syl	|- ( ph -> Fun G )
23		funco	|- ( ( Fun F /\ Fun G ) -> Fun ( F o. G ) )
24	20 22 23	syl2anc	|- ( ph -> Fun ( F o. G ) )
25		funisfsupp	|- ( ( Fun ( F o. G ) /\ ( F o. G ) e. _V /\ Z e. W ) -> ( ( F o. G ) finSupp Z <-> ( ( F o. G ) supp Z ) e. Fin ) )
26	24 9 3 25	syl3anc	|- ( ph -> ( ( F o. G ) finSupp Z <-> ( ( F o. G ) supp Z ) e. Fin ) )
27	17 26	mpbird	|- ( ph -> ( F o. G ) finSupp Z )