This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )