Theorem resfsupp

Description: If the restriction of a function by a set which, subtracted from the domain of the function so that its difference is finitely supported, the function itself is finitely supported. (Contributed by AV, 27-May-2019)

	Ref	Expression
Hypotheses	resfsupp.b	|- ( ph -> ( dom F \ B ) e. Fin )
	resfsupp.e	|- ( ph -> F e. W )
	resfsupp.f	|- ( ph -> Fun F )
	resfsupp.g	|- ( ph -> G = ( F |` B ) )
	resfsupp.s	|- ( ph -> G finSupp Z )
	resfsupp.z	|- ( ph -> Z e. V )
Assertion	resfsupp	|- ( ph -> F finSupp Z )

Proof

Step	Hyp	Ref	Expression
1		resfsupp.b	|- ( ph -> ( dom F \ B ) e. Fin )
2		resfsupp.e	|- ( ph -> F e. W )
3		resfsupp.f	|- ( ph -> Fun F )
4		resfsupp.g	|- ( ph -> G = ( F |` B ) )
5		resfsupp.s	|- ( ph -> G finSupp Z )
6		resfsupp.z	|- ( ph -> Z e. V )
7	5	fsuppimpd	|- ( ph -> ( G supp Z ) e. Fin )
8	1 2 4 7 6	ressuppfi	|- ( ph -> ( F supp Z ) e. Fin )
9		funisfsupp	|- ( ( Fun F /\ F e. W /\ Z e. V ) -> ( F finSupp Z <-> ( F supp Z ) e. Fin ) )
10	3 2 6 9	syl3anc	|- ( ph -> ( F finSupp Z <-> ( F supp Z ) e. Fin ) )
11	8 10	mpbird	|- ( ph -> F finSupp Z )