Step |
Hyp |
Ref |
Expression |
0 |
|
c2ndf |
⊢ 2ndF |
1 |
|
vr |
⊢ 𝑟 |
2 |
|
ccat |
⊢ Cat |
3 |
|
vs |
⊢ 𝑠 |
4 |
|
cbs |
⊢ Base |
5 |
1
|
cv |
⊢ 𝑟 |
6 |
5 4
|
cfv |
⊢ ( Base ‘ 𝑟 ) |
7 |
3
|
cv |
⊢ 𝑠 |
8 |
7 4
|
cfv |
⊢ ( Base ‘ 𝑠 ) |
9 |
6 8
|
cxp |
⊢ ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑠 ) ) |
10 |
|
vb |
⊢ 𝑏 |
11 |
|
c2nd |
⊢ 2nd |
12 |
10
|
cv |
⊢ 𝑏 |
13 |
11 12
|
cres |
⊢ ( 2nd ↾ 𝑏 ) |
14 |
|
vx |
⊢ 𝑥 |
15 |
|
vy |
⊢ 𝑦 |
16 |
14
|
cv |
⊢ 𝑥 |
17 |
|
chom |
⊢ Hom |
18 |
|
cxpc |
⊢ ×c |
19 |
5 7 18
|
co |
⊢ ( 𝑟 ×c 𝑠 ) |
20 |
19 17
|
cfv |
⊢ ( Hom ‘ ( 𝑟 ×c 𝑠 ) ) |
21 |
15
|
cv |
⊢ 𝑦 |
22 |
16 21 20
|
co |
⊢ ( 𝑥 ( Hom ‘ ( 𝑟 ×c 𝑠 ) ) 𝑦 ) |
23 |
11 22
|
cres |
⊢ ( 2nd ↾ ( 𝑥 ( Hom ‘ ( 𝑟 ×c 𝑠 ) ) 𝑦 ) ) |
24 |
14 15 12 12 23
|
cmpo |
⊢ ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ ( 𝑟 ×c 𝑠 ) ) 𝑦 ) ) ) |
25 |
13 24
|
cop |
⊢ 〈 ( 2nd ↾ 𝑏 ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ ( 𝑟 ×c 𝑠 ) ) 𝑦 ) ) ) 〉 |
26 |
10 9 25
|
csb |
⊢ ⦋ ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑠 ) ) / 𝑏 ⦌ 〈 ( 2nd ↾ 𝑏 ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ ( 𝑟 ×c 𝑠 ) ) 𝑦 ) ) ) 〉 |
27 |
1 3 2 2 26
|
cmpo |
⊢ ( 𝑟 ∈ Cat , 𝑠 ∈ Cat ↦ ⦋ ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑠 ) ) / 𝑏 ⦌ 〈 ( 2nd ↾ 𝑏 ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ ( 𝑟 ×c 𝑠 ) ) 𝑦 ) ) ) 〉 ) |
28 |
0 27
|
wceq |
⊢ 2ndF = ( 𝑟 ∈ Cat , 𝑠 ∈ Cat ↦ ⦋ ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑠 ) ) / 𝑏 ⦌ 〈 ( 2nd ↾ 𝑏 ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ ( 𝑟 ×c 𝑠 ) ) 𝑦 ) ) ) 〉 ) |