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 = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }
	dprdff.1	|- ( ph -> G dom DProd S )
	dprdff.2	|- ( ph -> dom S = I )
	dprdff.3	|- ( ph -> F e. W )
Assertion	dprdfcl	|- ( ( ph /\ X e. I ) -> ( F ` X ) e. ( S ` X ) )

Proof

Step	Hyp	Ref	Expression
1		dprdff.w	|- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }
2		dprdff.1	|- ( ph -> G dom DProd S )
3		dprdff.2	|- ( ph -> dom S = I )
4		dprdff.3	|- ( ph -> F e. W )
5	1 2 3	dprdw	|- ( ph -> ( F e. W <-> ( F Fn I /\ A. x e. I ( F ` x ) e. ( S ` x ) /\ F finSupp .0. ) ) )
6	4 5	mpbid	|- ( ph -> ( F Fn I /\ A. x e. I ( F ` x ) e. ( S ` x ) /\ F finSupp .0. ) )
7	6	simp2d	|- ( ph -> A. x e. I ( F ` x ) e. ( S ` x ) )
8		fveq2	|- ( x = X -> ( F ` x ) = ( F ` X ) )
9		fveq2	|- ( x = X -> ( S ` x ) = ( S ` X ) )
10	8 9	eleq12d	|- ( x = X -> ( ( F ` x ) e. ( S ` x ) <-> ( F ` X ) e. ( S ` X ) ) )
11	10	rspccva	|- ( ( A. x e. I ( F ` x ) e. ( S ` x ) /\ X e. I ) -> ( F ` X ) e. ( S ` X ) )
12	7 11	sylan	|- ( ( ph /\ X e. I ) -> ( F ` X ) e. ( S ` X ) )