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 |
1 2 3 4 5
|
prfval |
⊢ ( 𝜑 → 𝑃 = 〈 ( 𝑥 ∈ 𝐵 ↦ 〈 ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) 〉 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ℎ ∈ ( 𝑥 𝐻 𝑦 ) ↦ 〈 ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) 〉 ) ) 〉 ) |
9 |
2
|
fvexi |
⊢ 𝐵 ∈ V |
10 |
9
|
mptex |
⊢ ( 𝑥 ∈ 𝐵 ↦ 〈 ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) 〉 ) ∈ V |
11 |
9 9
|
mpoex |
⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ℎ ∈ ( 𝑥 𝐻 𝑦 ) ↦ 〈 ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) 〉 ) ) ∈ V |
12 |
10 11
|
op2ndd |
⊢ ( 𝑃 = 〈 ( 𝑥 ∈ 𝐵 ↦ 〈 ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) 〉 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ℎ ∈ ( 𝑥 𝐻 𝑦 ) ↦ 〈 ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) 〉 ) ) 〉 → ( 2nd ‘ 𝑃 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ℎ ∈ ( 𝑥 𝐻 𝑦 ) ↦ 〈 ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) 〉 ) ) ) |
13 |
8 12
|
syl |
⊢ ( 𝜑 → ( 2nd ‘ 𝑃 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ℎ ∈ ( 𝑥 𝐻 𝑦 ) ↦ 〈 ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) 〉 ) ) ) |
14 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → 𝑥 = 𝑋 ) |
15 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → 𝑦 = 𝑌 ) |
16 |
14 15
|
oveq12d |
⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑋 𝐻 𝑌 ) ) |
17 |
14 15
|
oveq12d |
⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) = ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑌 ) ) |
18 |
17
|
fveq1d |
⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) = ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑌 ) ‘ ℎ ) ) |
19 |
14 15
|
oveq12d |
⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) = ( 𝑋 ( 2nd ‘ 𝐺 ) 𝑌 ) ) |
20 |
19
|
fveq1d |
⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) = ( ( 𝑋 ( 2nd ‘ 𝐺 ) 𝑌 ) ‘ ℎ ) ) |
21 |
18 20
|
opeq12d |
⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → 〈 ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) 〉 = 〈 ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑌 ) ‘ ℎ ) , ( ( 𝑋 ( 2nd ‘ 𝐺 ) 𝑌 ) ‘ ℎ ) 〉 ) |
22 |
16 21
|
mpteq12dv |
⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( ℎ ∈ ( 𝑥 𝐻 𝑦 ) ↦ 〈 ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) 〉 ) = ( ℎ ∈ ( 𝑋 𝐻 𝑌 ) ↦ 〈 ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑌 ) ‘ ℎ ) , ( ( 𝑋 ( 2nd ‘ 𝐺 ) 𝑌 ) ‘ ℎ ) 〉 ) ) |
23 |
|
ovex |
⊢ ( 𝑋 𝐻 𝑌 ) ∈ V |
24 |
23
|
mptex |
⊢ ( ℎ ∈ ( 𝑋 𝐻 𝑌 ) ↦ 〈 ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑌 ) ‘ ℎ ) , ( ( 𝑋 ( 2nd ‘ 𝐺 ) 𝑌 ) ‘ ℎ ) 〉 ) ∈ V |
25 |
24
|
a1i |
⊢ ( 𝜑 → ( ℎ ∈ ( 𝑋 𝐻 𝑌 ) ↦ 〈 ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑌 ) ‘ ℎ ) , ( ( 𝑋 ( 2nd ‘ 𝐺 ) 𝑌 ) ‘ ℎ ) 〉 ) ∈ V ) |
26 |
13 22 6 7 25
|
ovmpod |
⊢ ( 𝜑 → ( 𝑋 ( 2nd ‘ 𝑃 ) 𝑌 ) = ( ℎ ∈ ( 𝑋 𝐻 𝑌 ) ↦ 〈 ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑌 ) ‘ ℎ ) , ( ( 𝑋 ( 2nd ‘ 𝐺 ) 𝑌 ) ‘ ℎ ) 〉 ) ) |