Step |
Hyp |
Ref |
Expression |
1 |
|
prfval.k |
⊢ 𝑃 = ( 𝐹 〈,〉F 𝐺 ) |
2 |
|
prfval.b |
⊢ 𝐵 = ( Base ‘ 𝐶 ) |
3 |
|
prfval.h |
⊢ 𝐻 = ( Hom ‘ 𝐶 ) |
4 |
|
prfval.c |
⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) |
5 |
|
prfval.d |
⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐸 ) ) |
6 |
|
prf1.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝐵 ) |
7 |
|
prf2.y |
⊢ ( 𝜑 → 𝑌 ∈ 𝐵 ) |
8 |
|
prf2.k |
⊢ ( 𝜑 → 𝐾 ∈ ( 𝑋 𝐻 𝑌 ) ) |
9 |
1 2 3 4 5 6 7
|
prf2fval |
⊢ ( 𝜑 → ( 𝑋 ( 2nd ‘ 𝑃 ) 𝑌 ) = ( ℎ ∈ ( 𝑋 𝐻 𝑌 ) ↦ 〈 ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑌 ) ‘ ℎ ) , ( ( 𝑋 ( 2nd ‘ 𝐺 ) 𝑌 ) ‘ ℎ ) 〉 ) ) |
10 |
|
simpr |
⊢ ( ( 𝜑 ∧ ℎ = 𝐾 ) → ℎ = 𝐾 ) |
11 |
10
|
fveq2d |
⊢ ( ( 𝜑 ∧ ℎ = 𝐾 ) → ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑌 ) ‘ ℎ ) = ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑌 ) ‘ 𝐾 ) ) |
12 |
10
|
fveq2d |
⊢ ( ( 𝜑 ∧ ℎ = 𝐾 ) → ( ( 𝑋 ( 2nd ‘ 𝐺 ) 𝑌 ) ‘ ℎ ) = ( ( 𝑋 ( 2nd ‘ 𝐺 ) 𝑌 ) ‘ 𝐾 ) ) |
13 |
11 12
|
opeq12d |
⊢ ( ( 𝜑 ∧ ℎ = 𝐾 ) → 〈 ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑌 ) ‘ ℎ ) , ( ( 𝑋 ( 2nd ‘ 𝐺 ) 𝑌 ) ‘ ℎ ) 〉 = 〈 ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑌 ) ‘ 𝐾 ) , ( ( 𝑋 ( 2nd ‘ 𝐺 ) 𝑌 ) ‘ 𝐾 ) 〉 ) |
14 |
|
opex |
⊢ 〈 ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑌 ) ‘ 𝐾 ) , ( ( 𝑋 ( 2nd ‘ 𝐺 ) 𝑌 ) ‘ 𝐾 ) 〉 ∈ V |
15 |
14
|
a1i |
⊢ ( 𝜑 → 〈 ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑌 ) ‘ 𝐾 ) , ( ( 𝑋 ( 2nd ‘ 𝐺 ) 𝑌 ) ‘ 𝐾 ) 〉 ∈ V ) |
16 |
9 13 8 15
|
fvmptd |
⊢ ( 𝜑 → ( ( 𝑋 ( 2nd ‘ 𝑃 ) 𝑌 ) ‘ 𝐾 ) = 〈 ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑌 ) ‘ 𝐾 ) , ( ( 𝑋 ( 2nd ‘ 𝐺 ) 𝑌 ) ‘ 𝐾 ) 〉 ) |