Theorem ressuppfi

Description: If the support of the restriction of a function by a set which, subtracted from the domain of the function so that its difference is finite, the support of the function itself is finite. (Contributed by AV, 22-Apr-2019)

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

Proof

Step	Hyp	Ref	Expression
1		ressuppfi.b	|- ( ph -> ( dom F \ B ) e. Fin )
2		ressuppfi.f	|- ( ph -> F e. W )
3		ressuppfi.g	|- ( ph -> G = ( F |` B ) )
4		ressuppfi.s	|- ( ph -> ( G supp Z ) e. Fin )
5		ressuppfi.z	|- ( ph -> Z e. V )
6	3	eqcomd	|- ( ph -> ( F |` B ) = G )
7	6	oveq1d	|- ( ph -> ( ( F |` B ) supp Z ) = ( G supp Z ) )
8	7 4	eqeltrd	|- ( ph -> ( ( F |` B ) supp Z ) e. Fin )
9		unfi	|- ( ( ( ( F |` B ) supp Z ) e. Fin /\ ( dom F \ B ) e. Fin ) -> ( ( ( F |` B ) supp Z ) u. ( dom F \ B ) ) e. Fin )
10	8 1 9	syl2anc	|- ( ph -> ( ( ( F |` B ) supp Z ) u. ( dom F \ B ) ) e. Fin )
11		ressuppssdif	|- ( ( F e. W /\ Z e. V ) -> ( F supp Z ) C_ ( ( ( F |` B ) supp Z ) u. ( dom F \ B ) ) )
12	2 5 11	syl2anc	|- ( ph -> ( F supp Z ) C_ ( ( ( F |` B ) supp Z ) u. ( dom F \ B ) ) )
13	10 12	ssfid	|- ( ph -> ( F supp Z ) e. Fin )