Theorem dprdwd

Description: A mapping being a finitely supported function in the family S . (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 11-Jul-2019) (Proof shortened by OpenAI, 30-Mar-2020)

	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 )
	dprdwd.3	|- ( ( ph /\ x e. I ) -> A e. ( S ` x ) )
	dprdwd.4	|- ( ph -> ( x e. I |-> A ) finSupp .0. )
Assertion	dprdwd	|- ( ph -> ( x e. I |-> A ) e. W )

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		dprdwd.3	|- ( ( ph /\ x e. I ) -> A e. ( S ` x ) )
5		dprdwd.4	|- ( ph -> ( x e. I |-> A ) finSupp .0. )
6		breq1	|- ( h = ( x e. I |-> A ) -> ( h finSupp .0. <-> ( x e. I |-> A ) finSupp .0. ) )
7	4	ralrimiva	|- ( ph -> A. x e. I A e. ( S ` x ) )
8	2 3	dprddomcld	|- ( ph -> I e. _V )
9		mptelixpg	|- ( I e. _V -> ( ( x e. I |-> A ) e. X_ x e. I ( S ` x ) <-> A. x e. I A e. ( S ` x ) ) )
10	8 9	syl	|- ( ph -> ( ( x e. I |-> A ) e. X_ x e. I ( S ` x ) <-> A. x e. I A e. ( S ` x ) ) )
11	7 10	mpbird	|- ( ph -> ( x e. I |-> A ) e. X_ x e. I ( S ` x ) )
12		fveq2	|- ( x = i -> ( S ` x ) = ( S ` i ) )
13	12	cbvixpv	|- X_ x e. I ( S ` x ) = X_ i e. I ( S ` i )
14	11 13	eleqtrdi	|- ( ph -> ( x e. I |-> A ) e. X_ i e. I ( S ` i ) )
15	6 14 5	elrabd	|- ( ph -> ( x e. I |-> A ) e. { h e. X_ i e. I ( S ` i ) | h finSupp .0. } )
16	15 1	eleqtrrdi	|- ( ph -> ( x e. I |-> A ) e. W )