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 |
1 2 3 4 5
|
prfval |
⊢ ( 𝜑 → 𝑃 = 〈 ( 𝑥 ∈ 𝐵 ↦ 〈 ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) 〉 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ℎ ∈ ( 𝑥 𝐻 𝑦 ) ↦ 〈 ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) 〉 ) ) 〉 ) |
8 |
2
|
fvexi |
⊢ 𝐵 ∈ V |
9 |
8
|
mptex |
⊢ ( 𝑥 ∈ 𝐵 ↦ 〈 ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) 〉 ) ∈ V |
10 |
8 8
|
mpoex |
⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ℎ ∈ ( 𝑥 𝐻 𝑦 ) ↦ 〈 ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) 〉 ) ) ∈ V |
11 |
9 10
|
op1std |
⊢ ( 𝑃 = 〈 ( 𝑥 ∈ 𝐵 ↦ 〈 ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) 〉 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ℎ ∈ ( 𝑥 𝐻 𝑦 ) ↦ 〈 ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) 〉 ) ) 〉 → ( 1st ‘ 𝑃 ) = ( 𝑥 ∈ 𝐵 ↦ 〈 ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) 〉 ) ) |
12 |
7 11
|
syl |
⊢ ( 𝜑 → ( 1st ‘ 𝑃 ) = ( 𝑥 ∈ 𝐵 ↦ 〈 ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) 〉 ) ) |
13 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝑥 = 𝑋 ) |
14 |
13
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) = ( ( 1st ‘ 𝐹 ) ‘ 𝑋 ) ) |
15 |
13
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) = ( ( 1st ‘ 𝐺 ) ‘ 𝑋 ) ) |
16 |
14 15
|
opeq12d |
⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 〈 ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) 〉 = 〈 ( ( 1st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑋 ) 〉 ) |
17 |
|
opex |
⊢ 〈 ( ( 1st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑋 ) 〉 ∈ V |
18 |
17
|
a1i |
⊢ ( 𝜑 → 〈 ( ( 1st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑋 ) 〉 ∈ V ) |
19 |
12 16 6 18
|
fvmptd |
⊢ ( 𝜑 → ( ( 1st ‘ 𝑃 ) ‘ 𝑋 ) = 〈 ( ( 1st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑋 ) 〉 ) |