Step |
Hyp |
Ref |
Expression |
0 |
|
ccomf |
⊢ compf |
1 |
|
vc |
⊢ 𝑐 |
2 |
|
cvv |
⊢ V |
3 |
|
vx |
⊢ 𝑥 |
4 |
|
cbs |
⊢ Base |
5 |
1
|
cv |
⊢ 𝑐 |
6 |
5 4
|
cfv |
⊢ ( Base ‘ 𝑐 ) |
7 |
6 6
|
cxp |
⊢ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑐 ) ) |
8 |
|
vy |
⊢ 𝑦 |
9 |
|
vg |
⊢ 𝑔 |
10 |
|
c2nd |
⊢ 2nd |
11 |
3
|
cv |
⊢ 𝑥 |
12 |
11 10
|
cfv |
⊢ ( 2nd ‘ 𝑥 ) |
13 |
|
chom |
⊢ Hom |
14 |
5 13
|
cfv |
⊢ ( Hom ‘ 𝑐 ) |
15 |
8
|
cv |
⊢ 𝑦 |
16 |
12 15 14
|
co |
⊢ ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) 𝑦 ) |
17 |
|
vf |
⊢ 𝑓 |
18 |
11 14
|
cfv |
⊢ ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) |
19 |
9
|
cv |
⊢ 𝑔 |
20 |
|
cco |
⊢ comp |
21 |
5 20
|
cfv |
⊢ ( comp ‘ 𝑐 ) |
22 |
11 15 21
|
co |
⊢ ( 𝑥 ( comp ‘ 𝑐 ) 𝑦 ) |
23 |
17
|
cv |
⊢ 𝑓 |
24 |
19 23 22
|
co |
⊢ ( 𝑔 ( 𝑥 ( comp ‘ 𝑐 ) 𝑦 ) 𝑓 ) |
25 |
9 17 16 18 24
|
cmpo |
⊢ ( 𝑔 ∈ ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ↦ ( 𝑔 ( 𝑥 ( comp ‘ 𝑐 ) 𝑦 ) 𝑓 ) ) |
26 |
3 8 7 6 25
|
cmpo |
⊢ ( 𝑥 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑐 ) ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ↦ ( 𝑔 ( 𝑥 ( comp ‘ 𝑐 ) 𝑦 ) 𝑓 ) ) ) |
27 |
1 2 26
|
cmpt |
⊢ ( 𝑐 ∈ V ↦ ( 𝑥 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑐 ) ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ↦ ( 𝑔 ( 𝑥 ( comp ‘ 𝑐 ) 𝑦 ) 𝑓 ) ) ) ) |
28 |
0 27
|
wceq |
⊢ compf = ( 𝑐 ∈ V ↦ ( 𝑥 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑐 ) ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ↦ ( 𝑔 ( 𝑥 ( comp ‘ 𝑐 ) 𝑦 ) 𝑓 ) ) ) ) |