Step |
Hyp |
Ref |
Expression |
0 |
|
cend |
⊢ End |
1 |
|
vc |
⊢ 𝑐 |
2 |
|
ccat |
⊢ Cat |
3 |
|
vx |
⊢ 𝑥 |
4 |
|
cbs |
⊢ Base |
5 |
1
|
cv |
⊢ 𝑐 |
6 |
5 4
|
cfv |
⊢ ( Base ‘ 𝑐 ) |
7 |
|
cnx |
⊢ ndx |
8 |
7 4
|
cfv |
⊢ ( Base ‘ ndx ) |
9 |
3
|
cv |
⊢ 𝑥 |
10 |
|
chom |
⊢ Hom |
11 |
5 10
|
cfv |
⊢ ( Hom ‘ 𝑐 ) |
12 |
9 9 11
|
co |
⊢ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑥 ) |
13 |
8 12
|
cop |
⊢ 〈 ( Base ‘ ndx ) , ( 𝑥 ( Hom ‘ 𝑐 ) 𝑥 ) 〉 |
14 |
|
cplusg |
⊢ +g |
15 |
7 14
|
cfv |
⊢ ( +g ‘ ndx ) |
16 |
9 9
|
cop |
⊢ 〈 𝑥 , 𝑥 〉 |
17 |
|
cco |
⊢ comp |
18 |
5 17
|
cfv |
⊢ ( comp ‘ 𝑐 ) |
19 |
16 9 18
|
co |
⊢ ( 〈 𝑥 , 𝑥 〉 ( comp ‘ 𝑐 ) 𝑥 ) |
20 |
15 19
|
cop |
⊢ 〈 ( +g ‘ ndx ) , ( 〈 𝑥 , 𝑥 〉 ( comp ‘ 𝑐 ) 𝑥 ) 〉 |
21 |
13 20
|
cpr |
⊢ { 〈 ( Base ‘ ndx ) , ( 𝑥 ( Hom ‘ 𝑐 ) 𝑥 ) 〉 , 〈 ( +g ‘ ndx ) , ( 〈 𝑥 , 𝑥 〉 ( comp ‘ 𝑐 ) 𝑥 ) 〉 } |
22 |
3 6 21
|
cmpt |
⊢ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ { 〈 ( Base ‘ ndx ) , ( 𝑥 ( Hom ‘ 𝑐 ) 𝑥 ) 〉 , 〈 ( +g ‘ ndx ) , ( 〈 𝑥 , 𝑥 〉 ( comp ‘ 𝑐 ) 𝑥 ) 〉 } ) |
23 |
1 2 22
|
cmpt |
⊢ ( 𝑐 ∈ Cat ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ { 〈 ( Base ‘ ndx ) , ( 𝑥 ( Hom ‘ 𝑐 ) 𝑥 ) 〉 , 〈 ( +g ‘ ndx ) , ( 〈 𝑥 , 𝑥 〉 ( comp ‘ 𝑐 ) 𝑥 ) 〉 } ) ) |
24 |
0 23
|
wceq |
⊢ End = ( 𝑐 ∈ Cat ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ { 〈 ( Base ‘ ndx ) , ( 𝑥 ( Hom ‘ 𝑐 ) 𝑥 ) 〉 , 〈 ( +g ‘ ndx ) , ( 〈 𝑥 , 𝑥 〉 ( comp ‘ 𝑐 ) 𝑥 ) 〉 } ) ) |