| Step |
Hyp |
Ref |
Expression |
| 1 |
|
psdval.s |
⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 ) |
| 2 |
|
psdval.b |
⊢ 𝐵 = ( Base ‘ 𝑆 ) |
| 3 |
|
psdval.d |
⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } |
| 4 |
|
psdval.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝐼 ) |
| 5 |
|
psdval.f |
⊢ ( 𝜑 → 𝐹 ∈ 𝐵 ) |
| 6 |
|
fveq1 |
⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) = ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) |
| 7 |
6
|
oveq2d |
⊢ ( 𝑓 = 𝐹 → ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) = ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) |
| 8 |
7
|
mpteq2dv |
⊢ ( 𝑓 = 𝐹 → ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) = ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) ) |
| 9 |
|
reldmpsr |
⊢ Rel dom mPwSer |
| 10 |
9 1 2
|
elbasov |
⊢ ( 𝐹 ∈ 𝐵 → ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ) |
| 11 |
5 10
|
syl |
⊢ ( 𝜑 → ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ) |
| 12 |
11
|
simpld |
⊢ ( 𝜑 → 𝐼 ∈ V ) |
| 13 |
11
|
simprd |
⊢ ( 𝜑 → 𝑅 ∈ V ) |
| 14 |
1 2 3 12 13 4
|
psdfval |
⊢ ( 𝜑 → ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) = ( 𝑓 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝑓 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) ) ) |
| 15 |
|
ovex |
⊢ ( ℕ0 ↑m 𝐼 ) ∈ V |
| 16 |
3 15
|
rabex2 |
⊢ 𝐷 ∈ V |
| 17 |
16
|
mptex |
⊢ ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) ∈ V |
| 18 |
17
|
a1i |
⊢ ( 𝜑 → ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) ∈ V ) |
| 19 |
8 14 5 18
|
fvmptd4 |
⊢ ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) = ( 𝑘 ∈ 𝐷 ↦ ( ( ( 𝑘 ‘ 𝑋 ) + 1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑘 ∘f + ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) ) |