This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )