Metamath Proof Explorer


Definition df-cofu

Description: Define the composition of two functors. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Assertion df-cofu func = g V , f V 1 st g 1 st f x dom dom 2 nd f , y dom dom 2 nd f 1 st f x 2 nd g 1 st f y x 2 nd f y

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccofu class func
1 vg setvar g
2 cvv class V
3 vf setvar f
4 c1st class 1 st
5 1 cv setvar g
6 5 4 cfv class 1 st g
7 3 cv setvar f
8 7 4 cfv class 1 st f
9 6 8 ccom class 1 st g 1 st f
10 vx setvar x
11 c2nd class 2 nd
12 7 11 cfv class 2 nd f
13 12 cdm class dom 2 nd f
14 13 cdm class dom dom 2 nd f
15 vy setvar y
16 10 cv setvar x
17 16 8 cfv class 1 st f x
18 5 11 cfv class 2 nd g
19 15 cv setvar y
20 19 8 cfv class 1 st f y
21 17 20 18 co class 1 st f x 2 nd g 1 st f y
22 16 19 12 co class x 2 nd f y
23 21 22 ccom class 1 st f x 2 nd g 1 st f y x 2 nd f y
24 10 15 14 14 23 cmpo class x dom dom 2 nd f , y dom dom 2 nd f 1 st f x 2 nd g 1 st f y x 2 nd f y
25 9 24 cop class 1 st g 1 st f x dom dom 2 nd f , y dom dom 2 nd f 1 st f x 2 nd g 1 st f y x 2 nd f y
26 1 3 2 2 25 cmpo class g V , f V 1 st g 1 st f x dom dom 2 nd f , y dom dom 2 nd f 1 st f x 2 nd g 1 st f y x 2 nd f y
27 0 26 wceq wff func = g V , f V 1 st g 1 st f x dom dom 2 nd f , y dom dom 2 nd f 1 st f x 2 nd g 1 st f y x 2 nd f y