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 𝑍 )