Theorem dprdffsupp

Description: A finitely supported function in S is a finitely supported function. (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 11-Jul-2019)

	Ref	Expression
Hypotheses	dprdff.w	$$⊢W=\left\{h\in \underset{i\in I}{⨉}S\left(i\right)|{finSupp}_{\underset{\dot{}}{0}}\left(h\right)\right\}$$
	dprdff.1	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}S$$
	dprdff.2	$$⊢\phi \to \mathrm{dom}S=I$$
	dprdff.3	$$⊢\phi \to F\in W$$
Assertion	dprdffsupp	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		dprdff.w	$$⊢W=\left\{h\in \underset{i\in I}{⨉}S\left(i\right)|{finSupp}_{\underset{\dot{}}{0}}\left(h\right)\right\}$$
2		dprdff.1	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}S$$
3		dprdff.2	$$⊢\phi \to \mathrm{dom}S=I$$
4		dprdff.3	$$⊢\phi \to F\in W$$
5	1 2 3	dprdw	$$⊢\phi \to \left(F\in W\leftrightarrow \left(FFnI\wedge \forall x\in IF\left(x\right)\in S\left(x\right)\wedge {finSupp}_{\underset{\dot{}}{0}}\left(F\right)\right)\right)$$
6	4 5	mpbid	$$⊢\phi \to \left(FFnI\wedge \forall x\in IF\left(x\right)\in S\left(x\right)\wedge {finSupp}_{\underset{\dot{}}{0}}\left(F\right)\right)$$
7	6	simp3d	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$