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	⊢ ( 𝜑 → ( dom 𝐹 ∖ 𝐵 ) ∈ Fin )
	ressuppfi.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑊 )
	ressuppfi.g	⊢ ( 𝜑 → 𝐺 = ( 𝐹 ↾ 𝐵 ) )
	ressuppfi.s	⊢ ( 𝜑 → ( 𝐺 supp 𝑍 ) ∈ Fin )
	ressuppfi.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
Assertion	ressuppfi	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		ressuppfi.b	⊢ ( 𝜑 → ( dom 𝐹 ∖ 𝐵 ) ∈ Fin )
2		ressuppfi.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑊 )
3		ressuppfi.g	⊢ ( 𝜑 → 𝐺 = ( 𝐹 ↾ 𝐵 ) )
4		ressuppfi.s	⊢ ( 𝜑 → ( 𝐺 supp 𝑍 ) ∈ Fin )
5		ressuppfi.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
6	3	eqcomd	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐵 ) = 𝐺 )
7	6	oveq1d	⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐵 ) supp 𝑍 ) = ( 𝐺 supp 𝑍 ) )
8	7 4	eqeltrd	⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐵 ) supp 𝑍 ) ∈ Fin )
9		unfi	⊢ ( ( ( ( 𝐹 ↾ 𝐵 ) supp 𝑍 ) ∈ Fin ∧ ( dom 𝐹 ∖ 𝐵 ) ∈ Fin ) → ( ( ( 𝐹 ↾ 𝐵 ) supp 𝑍 ) ∪ ( dom 𝐹 ∖ 𝐵 ) ) ∈ Fin )
10	8 1 9	syl2anc	⊢ ( 𝜑 → ( ( ( 𝐹 ↾ 𝐵 ) supp 𝑍 ) ∪ ( dom 𝐹 ∖ 𝐵 ) ) ∈ Fin )
11		ressuppssdif	⊢ ( ( 𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) → ( 𝐹 supp 𝑍 ) ⊆ ( ( ( 𝐹 ↾ 𝐵 ) supp 𝑍 ) ∪ ( dom 𝐹 ∖ 𝐵 ) ) )
12	2 5 11	syl2anc	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ ( ( ( 𝐹 ↾ 𝐵 ) supp 𝑍 ) ∪ ( dom 𝐹 ∖ 𝐵 ) ) )
13	10 12	ssfid	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ∈ Fin )