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