Metamath Proof Explorer


Theorem cofuval

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

Ref Expression
Hypotheses cofuval.b B = Base C
cofuval.f φ F C Func D
cofuval.g φ G D Func E
Assertion cofuval φ G func F = 1 st G 1 st F x B , y B 1 st F x 2 nd G 1 st F y x 2 nd F y

Proof

Step Hyp Ref Expression
1 cofuval.b B = Base C
2 cofuval.f φ F C Func D
3 cofuval.g φ G D Func E
4 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
5 4 a1i φ 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
6 simprl φ g = G f = F g = G
7 6 fveq2d φ g = G f = F 1 st g = 1 st G
8 simprr φ g = G f = F f = F
9 8 fveq2d φ g = G f = F 1 st f = 1 st F
10 7 9 coeq12d φ g = G f = F 1 st g 1 st f = 1 st G 1 st F
11 8 fveq2d φ g = G f = F 2 nd f = 2 nd F
12 11 dmeqd φ g = G f = F dom 2 nd f = dom 2 nd F
13 relfunc Rel C Func D
14 1st2ndbr Rel C Func D F C Func D 1 st F C Func D 2 nd F
15 13 2 14 sylancr φ 1 st F C Func D 2 nd F
16 1 15 funcfn2 φ 2 nd F Fn B × B
17 16 fndmd φ dom 2 nd F = B × B
18 17 adantr φ g = G f = F dom 2 nd F = B × B
19 12 18 eqtrd φ g = G f = F dom 2 nd f = B × B
20 19 dmeqd φ g = G f = F dom dom 2 nd f = dom B × B
21 dmxpid dom B × B = B
22 20 21 eqtrdi φ g = G f = F dom dom 2 nd f = B
23 6 fveq2d φ g = G f = F 2 nd g = 2 nd G
24 9 fveq1d φ g = G f = F 1 st f x = 1 st F x
25 9 fveq1d φ g = G f = F 1 st f y = 1 st F y
26 23 24 25 oveq123d φ g = G f = F 1 st f x 2 nd g 1 st f y = 1 st F x 2 nd G 1 st F y
27 11 oveqd φ g = G f = F x 2 nd f y = x 2 nd F y
28 26 27 coeq12d φ g = G f = F 1 st f x 2 nd g 1 st f y x 2 nd f y = 1 st F x 2 nd G 1 st F y x 2 nd F y
29 22 22 28 mpoeq123dv φ g = G f = 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 = x B , y B 1 st F x 2 nd G 1 st F y x 2 nd F y
30 10 29 opeq12d φ g = G f = F 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 = 1 st G 1 st F x B , y B 1 st F x 2 nd G 1 st F y x 2 nd F y
31 3 elexd φ G V
32 2 elexd φ F V
33 opex 1 st G 1 st F x B , y B 1 st F x 2 nd G 1 st F y x 2 nd F y V
34 33 a1i φ 1 st G 1 st F x B , y B 1 st F x 2 nd G 1 st F y x 2 nd F y V
35 5 30 31 32 34 ovmpod φ G func F = 1 st G 1 st F x B , y B 1 st F x 2 nd G 1 st F y x 2 nd F y