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

Metamath Proof Explorer

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 )