Theorem fsuppunfi

Description: The union of the support of two finitely supported functions is finite. (Contributed by AV, 1-Jul-2019)

	Ref	Expression
Hypotheses	fsuppun.f	⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )
	fsuppun.g	⊢ ( 𝜑 → 𝐺 finSupp 𝑍 )
Assertion	fsuppunfi	⊢ ( 𝜑 → ( ( 𝐹 supp 𝑍 ) ∪ ( 𝐺 supp 𝑍 ) ) ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		fsuppun.f	⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )
2		fsuppun.g	⊢ ( 𝜑 → 𝐺 finSupp 𝑍 )
3		fsuppimp	⊢ ( 𝐹 finSupp 𝑍 → ( Fun 𝐹 ∧ ( 𝐹 supp 𝑍 ) ∈ Fin ) )
4		fsuppimp	⊢ ( 𝐺 finSupp 𝑍 → ( Fun 𝐺 ∧ ( 𝐺 supp 𝑍 ) ∈ Fin ) )
5		unfi	⊢ ( ( ( 𝐹 supp 𝑍 ) ∈ Fin ∧ ( 𝐺 supp 𝑍 ) ∈ Fin ) → ( ( 𝐹 supp 𝑍 ) ∪ ( 𝐺 supp 𝑍 ) ) ∈ Fin )
6	5	expcom	⊢ ( ( 𝐺 supp 𝑍 ) ∈ Fin → ( ( 𝐹 supp 𝑍 ) ∈ Fin → ( ( 𝐹 supp 𝑍 ) ∪ ( 𝐺 supp 𝑍 ) ) ∈ Fin ) )
7	6	adantl	⊢ ( ( Fun 𝐺 ∧ ( 𝐺 supp 𝑍 ) ∈ Fin ) → ( ( 𝐹 supp 𝑍 ) ∈ Fin → ( ( 𝐹 supp 𝑍 ) ∪ ( 𝐺 supp 𝑍 ) ) ∈ Fin ) )
8	2 4 7	3syl	⊢ ( 𝜑 → ( ( 𝐹 supp 𝑍 ) ∈ Fin → ( ( 𝐹 supp 𝑍 ) ∪ ( 𝐺 supp 𝑍 ) ) ∈ Fin ) )
9	8	com12	⊢ ( ( 𝐹 supp 𝑍 ) ∈ Fin → ( 𝜑 → ( ( 𝐹 supp 𝑍 ) ∪ ( 𝐺 supp 𝑍 ) ) ∈ Fin ) )
10	3 9	simpl2im	⊢ ( 𝐹 finSupp 𝑍 → ( 𝜑 → ( ( 𝐹 supp 𝑍 ) ∪ ( 𝐺 supp 𝑍 ) ) ∈ Fin ) )
11	1 10	mpcom	⊢ ( 𝜑 → ( ( 𝐹 supp 𝑍 ) ∪ ( 𝐺 supp 𝑍 ) ) ∈ Fin )