Metamath Proof Explorer


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