Step |
Hyp |
Ref |
Expression |
1 |
|
xpccat.t |
⊢ 𝑇 = ( 𝐶 ×c 𝐷 ) |
2 |
|
xpccat.c |
⊢ ( 𝜑 → 𝐶 ∈ Cat ) |
3 |
|
xpccat.d |
⊢ ( 𝜑 → 𝐷 ∈ Cat ) |
4 |
|
xpccat.x |
⊢ 𝑋 = ( Base ‘ 𝐶 ) |
5 |
|
xpccat.y |
⊢ 𝑌 = ( Base ‘ 𝐷 ) |
6 |
|
xpccat.i |
⊢ 𝐼 = ( Id ‘ 𝐶 ) |
7 |
|
xpccat.j |
⊢ 𝐽 = ( Id ‘ 𝐷 ) |
8 |
|
xpcid.1 |
⊢ 1 = ( Id ‘ 𝑇 ) |
9 |
|
xpcid.r |
⊢ ( 𝜑 → 𝑅 ∈ 𝑋 ) |
10 |
|
xpcid.s |
⊢ ( 𝜑 → 𝑆 ∈ 𝑌 ) |
11 |
|
df-ov |
⊢ ( 𝑅 1 𝑆 ) = ( 1 ‘ 〈 𝑅 , 𝑆 〉 ) |
12 |
1 2 3 4 5 6 7
|
xpccatid |
⊢ ( 𝜑 → ( 𝑇 ∈ Cat ∧ ( Id ‘ 𝑇 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 〈 ( 𝐼 ‘ 𝑥 ) , ( 𝐽 ‘ 𝑦 ) 〉 ) ) ) |
13 |
12
|
simprd |
⊢ ( 𝜑 → ( Id ‘ 𝑇 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 〈 ( 𝐼 ‘ 𝑥 ) , ( 𝐽 ‘ 𝑦 ) 〉 ) ) |
14 |
8 13
|
eqtrid |
⊢ ( 𝜑 → 1 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 〈 ( 𝐼 ‘ 𝑥 ) , ( 𝐽 ‘ 𝑦 ) 〉 ) ) |
15 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑅 ∧ 𝑦 = 𝑆 ) ) → 𝑥 = 𝑅 ) |
16 |
15
|
fveq2d |
⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑅 ∧ 𝑦 = 𝑆 ) ) → ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑅 ) ) |
17 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑅 ∧ 𝑦 = 𝑆 ) ) → 𝑦 = 𝑆 ) |
18 |
17
|
fveq2d |
⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑅 ∧ 𝑦 = 𝑆 ) ) → ( 𝐽 ‘ 𝑦 ) = ( 𝐽 ‘ 𝑆 ) ) |
19 |
16 18
|
opeq12d |
⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑅 ∧ 𝑦 = 𝑆 ) ) → 〈 ( 𝐼 ‘ 𝑥 ) , ( 𝐽 ‘ 𝑦 ) 〉 = 〈 ( 𝐼 ‘ 𝑅 ) , ( 𝐽 ‘ 𝑆 ) 〉 ) |
20 |
|
opex |
⊢ 〈 ( 𝐼 ‘ 𝑅 ) , ( 𝐽 ‘ 𝑆 ) 〉 ∈ V |
21 |
20
|
a1i |
⊢ ( 𝜑 → 〈 ( 𝐼 ‘ 𝑅 ) , ( 𝐽 ‘ 𝑆 ) 〉 ∈ V ) |
22 |
14 19 9 10 21
|
ovmpod |
⊢ ( 𝜑 → ( 𝑅 1 𝑆 ) = 〈 ( 𝐼 ‘ 𝑅 ) , ( 𝐽 ‘ 𝑆 ) 〉 ) |
23 |
11 22
|
eqtr3id |
⊢ ( 𝜑 → ( 1 ‘ 〈 𝑅 , 𝑆 〉 ) = 〈 ( 𝐼 ‘ 𝑅 ) , ( 𝐽 ‘ 𝑆 ) 〉 ) |