Step |
Hyp |
Ref |
Expression |
1 |
|
tendoi.i |
⊢ 𝐼 = ( 𝑠 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ◡ ( 𝑠 ‘ 𝑓 ) ) ) |
2 |
|
fveq1 |
⊢ ( 𝑠 = 𝑢 → ( 𝑠 ‘ 𝑓 ) = ( 𝑢 ‘ 𝑓 ) ) |
3 |
2
|
cnveqd |
⊢ ( 𝑠 = 𝑢 → ◡ ( 𝑠 ‘ 𝑓 ) = ◡ ( 𝑢 ‘ 𝑓 ) ) |
4 |
3
|
mpteq2dv |
⊢ ( 𝑠 = 𝑢 → ( 𝑓 ∈ 𝑇 ↦ ◡ ( 𝑠 ‘ 𝑓 ) ) = ( 𝑓 ∈ 𝑇 ↦ ◡ ( 𝑢 ‘ 𝑓 ) ) ) |
5 |
|
fveq2 |
⊢ ( 𝑓 = 𝑔 → ( 𝑢 ‘ 𝑓 ) = ( 𝑢 ‘ 𝑔 ) ) |
6 |
5
|
cnveqd |
⊢ ( 𝑓 = 𝑔 → ◡ ( 𝑢 ‘ 𝑓 ) = ◡ ( 𝑢 ‘ 𝑔 ) ) |
7 |
6
|
cbvmptv |
⊢ ( 𝑓 ∈ 𝑇 ↦ ◡ ( 𝑢 ‘ 𝑓 ) ) = ( 𝑔 ∈ 𝑇 ↦ ◡ ( 𝑢 ‘ 𝑔 ) ) |
8 |
4 7
|
eqtrdi |
⊢ ( 𝑠 = 𝑢 → ( 𝑓 ∈ 𝑇 ↦ ◡ ( 𝑠 ‘ 𝑓 ) ) = ( 𝑔 ∈ 𝑇 ↦ ◡ ( 𝑢 ‘ 𝑔 ) ) ) |
9 |
8
|
cbvmptv |
⊢ ( 𝑠 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ◡ ( 𝑠 ‘ 𝑓 ) ) ) = ( 𝑢 ∈ 𝐸 ↦ ( 𝑔 ∈ 𝑇 ↦ ◡ ( 𝑢 ‘ 𝑔 ) ) ) |
10 |
1 9
|
eqtri |
⊢ 𝐼 = ( 𝑢 ∈ 𝐸 ↦ ( 𝑔 ∈ 𝑇 ↦ ◡ ( 𝑢 ‘ 𝑔 ) ) ) |