Theorem dprdfcl

Description: A finitely supported function in S has its X -th element in S ( X ) . (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	dprdfcl	$$⊢\left(\phi \wedge X\in I\right)\to F\left(X\right)\in S\left(X\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	simp2d	$$⊢\phi \to \forall x\in IF\left(x\right)\in S\left(x\right)$$
8		fveq2	$$⊢x=X\to F\left(x\right)=F\left(X\right)$$
9		fveq2	$$⊢x=X\to S\left(x\right)=S\left(X\right)$$
10	8 9	eleq12d	$$⊢x=X\to \left(F\left(x\right)\in S\left(x\right)\leftrightarrow F\left(X\right)\in S\left(X\right)\right)$$
11	10	rspccva	$$⊢\left(\forall x\in IF\left(x\right)\in S\left(x\right)\wedge X\in I\right)\to F\left(X\right)\in S\left(X\right)$$
12	7 11	sylan	$$⊢\left(\phi \wedge X\in I\right)\to F\left(X\right)\in S\left(X\right)$$