| Step | Hyp | Ref | Expression | 
						
							| 1 |  | psdval.s |  |-  S = ( I mPwSer R ) | 
						
							| 2 |  | psdval.b |  |-  B = ( Base ` S ) | 
						
							| 3 |  | psdval.d |  |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | 
						
							| 4 |  | psdval.x |  |-  ( ph -> X e. I ) | 
						
							| 5 |  | psdval.f |  |-  ( ph -> F e. B ) | 
						
							| 6 |  | fveq1 |  |-  ( f = F -> ( f ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) = ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) | 
						
							| 7 | 6 | oveq2d |  |-  ( f = F -> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( f ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) = ( ( ( k ` X ) + 1 ) ( .g ` R ) ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) | 
						
							| 8 | 7 | mpteq2dv |  |-  ( f = F -> ( k e. D |-> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( f ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) = ( k e. D |-> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) ) | 
						
							| 9 |  | reldmpsr |  |-  Rel dom mPwSer | 
						
							| 10 | 9 1 2 | elbasov |  |-  ( F e. B -> ( I e. _V /\ R e. _V ) ) | 
						
							| 11 | 5 10 | syl |  |-  ( ph -> ( I e. _V /\ R e. _V ) ) | 
						
							| 12 | 11 | simpld |  |-  ( ph -> I e. _V ) | 
						
							| 13 | 11 | simprd |  |-  ( ph -> R e. _V ) | 
						
							| 14 | 1 2 3 12 13 4 | psdfval |  |-  ( ph -> ( ( I mPSDer R ) ` X ) = ( f e. B |-> ( k e. D |-> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( f ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) ) ) | 
						
							| 15 |  | ovex |  |-  ( NN0 ^m I ) e. _V | 
						
							| 16 | 3 15 | rabex2 |  |-  D e. _V | 
						
							| 17 | 16 | mptex |  |-  ( k e. D |-> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) e. _V | 
						
							| 18 | 17 | a1i |  |-  ( ph -> ( k e. D |-> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) e. _V ) | 
						
							| 19 | 8 14 5 18 | fvmptd4 |  |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` F ) = ( k e. D |-> ( ( ( k ` X ) + 1 ) ( .g ` R ) ( F ` ( k oF + ( y e. I |-> if ( y = X , 1 , 0 ) ) ) ) ) ) ) |