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

Metamath Proof Explorer

Theorem fsuppsssupp

Description: If the support of a function is a subset of the support of a finitely supported function, the function is finitely supported. (Contributed by AV, 2-Jul-2019) (Proof shortened by AV, 15-Jul-2019)

Ref Expression
Assertion fsuppsssupp ( ( ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ) ∧ ( 𝐹 finSupp 𝑍 ∧ ( 𝐺 supp 𝑍 ) ⊆ ( 𝐹 supp 𝑍 ) ) ) → 𝐺 finSupp 𝑍 )

Proof

Step Hyp Ref Expression
1 simpll ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ) ∧ ( 𝐹 finSupp 𝑍 ∧ ( 𝐺 supp 𝑍 ) ⊆ ( 𝐹 supp 𝑍 ) ) ) → 𝐺 ∈ 𝑉 )
2 simplr ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ) ∧ ( 𝐹 finSupp 𝑍 ∧ ( 𝐺 supp 𝑍 ) ⊆ ( 𝐹 supp 𝑍 ) ) ) → Fun 𝐺 )
3 relfsupp ⊢ Rel finSupp
4 3 brrelex2i ⊢ ( 𝐹 finSupp 𝑍 → 𝑍 ∈ V )
5 4 ad2antrl ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ) ∧ ( 𝐹 finSupp 𝑍 ∧ ( 𝐺 supp 𝑍 ) ⊆ ( 𝐹 supp 𝑍 ) ) ) → 𝑍 ∈ V )
6 id ⊢ ( 𝐹 finSupp 𝑍 → 𝐹 finSupp 𝑍 )
7 6 fsuppimpd ⊢ ( 𝐹 finSupp 𝑍 → ( 𝐹 supp 𝑍 ) ∈ Fin )
8 7 anim1i ⊢ ( ( 𝐹 finSupp 𝑍 ∧ ( 𝐺 supp 𝑍 ) ⊆ ( 𝐹 supp 𝑍 ) ) → ( ( 𝐹 supp 𝑍 ) ∈ Fin ∧ ( 𝐺 supp 𝑍 ) ⊆ ( 𝐹 supp 𝑍 ) ) )
9 8 adantl ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ) ∧ ( 𝐹 finSupp 𝑍 ∧ ( 𝐺 supp 𝑍 ) ⊆ ( 𝐹 supp 𝑍 ) ) ) → ( ( 𝐹 supp 𝑍 ) ∈ Fin ∧ ( 𝐺 supp 𝑍 ) ⊆ ( 𝐹 supp 𝑍 ) ) )
10 suppssfifsupp ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ∧ 𝑍 ∈ V ) ∧ ( ( 𝐹 supp 𝑍 ) ∈ Fin ∧ ( 𝐺 supp 𝑍 ) ⊆ ( 𝐹 supp 𝑍 ) ) ) → 𝐺 finSupp 𝑍 )
11 1 2 5 9 10 syl31anc ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ) ∧ ( 𝐹 finSupp 𝑍 ∧ ( 𝐺 supp 𝑍 ) ⊆ ( 𝐹 supp 𝑍 ) ) ) → 𝐺 finSupp 𝑍 )