Step |
Hyp |
Ref |
Expression |
1 |
|
diagval.l |
⊢ 𝐿 = ( 𝐶 Δfunc 𝐷 ) |
2 |
|
diagval.c |
⊢ ( 𝜑 → 𝐶 ∈ Cat ) |
3 |
|
diagval.d |
⊢ ( 𝜑 → 𝐷 ∈ Cat ) |
4 |
|
df-diag |
⊢ Δfunc = ( 𝑐 ∈ Cat , 𝑑 ∈ Cat ↦ ( 〈 𝑐 , 𝑑 〉 curryF ( 𝑐 1stF 𝑑 ) ) ) |
5 |
4
|
a1i |
⊢ ( 𝜑 → Δfunc = ( 𝑐 ∈ Cat , 𝑑 ∈ Cat ↦ ( 〈 𝑐 , 𝑑 〉 curryF ( 𝑐 1stF 𝑑 ) ) ) ) |
6 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ) → 𝑐 = 𝐶 ) |
7 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ) → 𝑑 = 𝐷 ) |
8 |
6 7
|
opeq12d |
⊢ ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ) → 〈 𝑐 , 𝑑 〉 = 〈 𝐶 , 𝐷 〉 ) |
9 |
6 7
|
oveq12d |
⊢ ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ) → ( 𝑐 1stF 𝑑 ) = ( 𝐶 1stF 𝐷 ) ) |
10 |
8 9
|
oveq12d |
⊢ ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ) → ( 〈 𝑐 , 𝑑 〉 curryF ( 𝑐 1stF 𝑑 ) ) = ( 〈 𝐶 , 𝐷 〉 curryF ( 𝐶 1stF 𝐷 ) ) ) |
11 |
|
ovexd |
⊢ ( 𝜑 → ( 〈 𝐶 , 𝐷 〉 curryF ( 𝐶 1stF 𝐷 ) ) ∈ V ) |
12 |
5 10 2 3 11
|
ovmpod |
⊢ ( 𝜑 → ( 𝐶 Δfunc 𝐷 ) = ( 〈 𝐶 , 𝐷 〉 curryF ( 𝐶 1stF 𝐷 ) ) ) |
13 |
1 12
|
syl5eq |
⊢ ( 𝜑 → 𝐿 = ( 〈 𝐶 , 𝐷 〉 curryF ( 𝐶 1stF 𝐷 ) ) ) |