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

Metamath Proof Explorer

Theorem suppssfifsupp

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

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

Proof

Step Hyp Ref Expression
1 ssfi ⊢ ( ( 𝐹 ∈ Fin ∧ ( 𝐺 supp 𝑍 ) ⊆ 𝐹 ) → ( 𝐺 supp 𝑍 ) ∈ Fin )
2 1 adantl ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝐹 ∈ Fin ∧ ( 𝐺 supp 𝑍 ) ⊆ 𝐹 ) ) → ( 𝐺 supp 𝑍 ) ∈ Fin )
3 3ancoma ⊢ ( ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ∧ 𝑍 ∈ 𝑊 ) ↔ ( Fun 𝐺 ∧ 𝐺 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) )
4 3 biimpi ⊢ ( ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ∧ 𝑍 ∈ 𝑊 ) → ( Fun 𝐺 ∧ 𝐺 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) )
5 4 adantr ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝐹 ∈ Fin ∧ ( 𝐺 supp 𝑍 ) ⊆ 𝐹 ) ) → ( Fun 𝐺 ∧ 𝐺 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) )
6 funisfsupp ⊢ ( ( Fun 𝐺 ∧ 𝐺 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐺 finSupp 𝑍 ↔ ( 𝐺 supp 𝑍 ) ∈ Fin ) )
7 5 6 syl ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝐹 ∈ Fin ∧ ( 𝐺 supp 𝑍 ) ⊆ 𝐹 ) ) → ( 𝐺 finSupp 𝑍 ↔ ( 𝐺 supp 𝑍 ) ∈ Fin ) )
8 2 7 mpbird ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝐹 ∈ Fin ∧ ( 𝐺 supp 𝑍 ) ⊆ 𝐹 ) ) → 𝐺 finSupp 𝑍 )