Metamath Proof Explorer


Theorem cofucl

Description: The composition of two functors is a functor. Proposition 3.23 of Adamek p. 33. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses cofucl.f φ F C Func D
cofucl.g φ G D Func E
Assertion cofucl φ G func F C Func E

Proof

Step Hyp Ref Expression
1 cofucl.f φ F C Func D
2 cofucl.g φ G D Func E
3 eqid Base C = Base C
4 3 1 2 cofuval φ G func F = 1 st G 1 st F x Base C , y Base C 1 st F x 2 nd G 1 st F y x 2 nd F y
5 3 1 2 cofu1st φ 1 st G func F = 1 st G 1 st F
6 4 fveq2d φ 2 nd G func F = 2 nd 1 st G 1 st F x Base C , y Base C 1 st F x 2 nd G 1 st F y x 2 nd F y
7 fvex 1 st G V
8 fvex 1 st F V
9 7 8 coex 1 st G 1 st F V
10 fvex Base C V
11 10 10 mpoex x Base C , y Base C 1 st F x 2 nd G 1 st F y x 2 nd F y V
12 9 11 op2nd 2 nd 1 st G 1 st F x Base C , y Base C 1 st F x 2 nd G 1 st F y x 2 nd F y = x Base C , y Base C 1 st F x 2 nd G 1 st F y x 2 nd F y
13 6 12 syl6eq φ 2 nd G func F = x Base C , y Base C 1 st F x 2 nd G 1 st F y x 2 nd F y
14 5 13 opeq12d φ 1 st G func F 2 nd G func F = 1 st G 1 st F x Base C , y Base C 1 st F x 2 nd G 1 st F y x 2 nd F y
15 4 14 eqtr4d φ G func F = 1 st G func F 2 nd G func F
16 eqid Base D = Base D
17 eqid Base E = Base E
18 relfunc Rel D Func E
19 1st2ndbr Rel D Func E G D Func E 1 st G D Func E 2 nd G
20 18 2 19 sylancr φ 1 st G D Func E 2 nd G
21 16 17 20 funcf1 φ 1 st G : Base D Base E
22 relfunc Rel C Func D
23 1st2ndbr Rel C Func D F C Func D 1 st F C Func D 2 nd F
24 22 1 23 sylancr φ 1 st F C Func D 2 nd F
25 3 16 24 funcf1 φ 1 st F : Base C Base D
26 fco 1 st G : Base D Base E 1 st F : Base C Base D 1 st G 1 st F : Base C Base E
27 21 25 26 syl2anc φ 1 st G 1 st F : Base C Base E
28 5 feq1d φ 1 st G func F : Base C Base E 1 st G 1 st F : Base C Base E
29 27 28 mpbird φ 1 st G func F : Base C Base E
30 eqid x Base C , y Base C 1 st F x 2 nd G 1 st F y x 2 nd F y = x Base C , y Base C 1 st F x 2 nd G 1 st F y x 2 nd F y
31 ovex 1 st F x 2 nd G 1 st F y V
32 ovex x 2 nd F y V
33 31 32 coex 1 st F x 2 nd G 1 st F y x 2 nd F y V
34 30 33 fnmpoi x Base C , y Base C 1 st F x 2 nd G 1 st F y x 2 nd F y Fn Base C × Base C
35 13 fneq1d φ 2 nd G func F Fn Base C × Base C x Base C , y Base C 1 st F x 2 nd G 1 st F y x 2 nd F y Fn Base C × Base C
36 34 35 mpbiri φ 2 nd G func F Fn Base C × Base C
37 eqid Hom D = Hom D
38 eqid Hom E = Hom E
39 20 adantr φ x Base C y Base C 1 st G D Func E 2 nd G
40 25 adantr φ x Base C y Base C 1 st F : Base C Base D
41 simprl φ x Base C y Base C x Base C
42 40 41 ffvelrnd φ x Base C y Base C 1 st F x Base D
43 simprr φ x Base C y Base C y Base C
44 40 43 ffvelrnd φ x Base C y Base C 1 st F y Base D
45 16 37 38 39 42 44 funcf2 φ x Base C y Base C 1 st F x 2 nd G 1 st F y : 1 st F x Hom D 1 st F y 1 st G 1 st F x Hom E 1 st G 1 st F y
46 eqid Hom C = Hom C
47 24 adantr φ x Base C y Base C 1 st F C Func D 2 nd F
48 3 46 37 47 41 43 funcf2 φ x Base C y Base C x 2 nd F y : x Hom C y 1 st F x Hom D 1 st F y
49 fco 1 st F x 2 nd G 1 st F y : 1 st F x Hom D 1 st F y 1 st G 1 st F x Hom E 1 st G 1 st F y x 2 nd F y : x Hom C y 1 st F x Hom D 1 st F y 1 st F x 2 nd G 1 st F y x 2 nd F y : x Hom C y 1 st G 1 st F x Hom E 1 st G 1 st F y
50 45 48 49 syl2anc φ x Base C y Base C 1 st F x 2 nd G 1 st F y x 2 nd F y : x Hom C y 1 st G 1 st F x Hom E 1 st G 1 st F y
51 ovex 1 st G 1 st F x Hom E 1 st G 1 st F y V
52 ovex x Hom C y V
53 51 52 elmap 1 st F x 2 nd G 1 st F y x 2 nd F y 1 st G 1 st F x Hom E 1 st G 1 st F y x Hom C y 1 st F x 2 nd G 1 st F y x 2 nd F y : x Hom C y 1 st G 1 st F x Hom E 1 st G 1 st F y
54 50 53 sylibr φ x Base C y Base C 1 st F x 2 nd G 1 st F y x 2 nd F y 1 st G 1 st F x Hom E 1 st G 1 st F y x Hom C y
55 1 adantr φ x Base C y Base C F C Func D
56 2 adantr φ x Base C y Base C G D Func E
57 3 55 56 41 43 cofu2nd φ x Base C y Base C x 2 nd G func F y = 1 st F x 2 nd G 1 st F y x 2 nd F y
58 3 55 56 41 cofu1 φ x Base C y Base C 1 st G func F x = 1 st G 1 st F x
59 3 55 56 43 cofu1 φ x Base C y Base C 1 st G func F y = 1 st G 1 st F y
60 58 59 oveq12d φ x Base C y Base C 1 st G func F x Hom E 1 st G func F y = 1 st G 1 st F x Hom E 1 st G 1 st F y
61 60 oveq1d φ x Base C y Base C 1 st G func F x Hom E 1 st G func F y x Hom C y = 1 st G 1 st F x Hom E 1 st G 1 st F y x Hom C y
62 54 57 61 3eltr4d φ x Base C y Base C x 2 nd G func F y 1 st G func F x Hom E 1 st G func F y x Hom C y
63 62 ralrimivva φ x Base C y Base C x 2 nd G func F y 1 st G func F x Hom E 1 st G func F y x Hom C y
64 fveq2 z = x y 2 nd G func F z = 2 nd G func F x y
65 df-ov x 2 nd G func F y = 2 nd G func F x y
66 64 65 syl6eqr z = x y 2 nd G func F z = x 2 nd G func F y
67 vex x V
68 vex y V
69 67 68 op1std z = x y 1 st z = x
70 69 fveq2d z = x y 1 st G func F 1 st z = 1 st G func F x
71 67 68 op2ndd z = x y 2 nd z = y
72 71 fveq2d z = x y 1 st G func F 2 nd z = 1 st G func F y
73 70 72 oveq12d z = x y 1 st G func F 1 st z Hom E 1 st G func F 2 nd z = 1 st G func F x Hom E 1 st G func F y
74 fveq2 z = x y Hom C z = Hom C x y
75 df-ov x Hom C y = Hom C x y
76 74 75 syl6eqr z = x y Hom C z = x Hom C y
77 73 76 oveq12d z = x y 1 st G func F 1 st z Hom E 1 st G func F 2 nd z Hom C z = 1 st G func F x Hom E 1 st G func F y x Hom C y
78 66 77 eleq12d z = x y 2 nd G func F z 1 st G func F 1 st z Hom E 1 st G func F 2 nd z Hom C z x 2 nd G func F y 1 st G func F x Hom E 1 st G func F y x Hom C y
79 78 ralxp z Base C × Base C 2 nd G func F z 1 st G func F 1 st z Hom E 1 st G func F 2 nd z Hom C z x Base C y Base C x 2 nd G func F y 1 st G func F x Hom E 1 st G func F y x Hom C y
80 63 79 sylibr φ z Base C × Base C 2 nd G func F z 1 st G func F 1 st z Hom E 1 st G func F 2 nd z Hom C z
81 fvex 2 nd G func F V
82 81 elixp 2 nd G func F z Base C × Base C 1 st G func F 1 st z Hom E 1 st G func F 2 nd z Hom C z 2 nd G func F Fn Base C × Base C z Base C × Base C 2 nd G func F z 1 st G func F 1 st z Hom E 1 st G func F 2 nd z Hom C z
83 36 80 82 sylanbrc φ 2 nd G func F z Base C × Base C 1 st G func F 1 st z Hom E 1 st G func F 2 nd z Hom C z
84 eqid Id C = Id C
85 eqid Id D = Id D
86 24 adantr φ x Base C 1 st F C Func D 2 nd F
87 simpr φ x Base C x Base C
88 3 84 85 86 87 funcid φ x Base C x 2 nd F x Id C x = Id D 1 st F x
89 88 fveq2d φ x Base C 1 st F x 2 nd G 1 st F x x 2 nd F x Id C x = 1 st F x 2 nd G 1 st F x Id D 1 st F x
90 eqid Id E = Id E
91 20 adantr φ x Base C 1 st G D Func E 2 nd G
92 25 ffvelrnda φ x Base C 1 st F x Base D
93 16 85 90 91 92 funcid φ x Base C 1 st F x 2 nd G 1 st F x Id D 1 st F x = Id E 1 st G 1 st F x
94 89 93 eqtrd φ x Base C 1 st F x 2 nd G 1 st F x x 2 nd F x Id C x = Id E 1 st G 1 st F x
95 1 adantr φ x Base C F C Func D
96 2 adantr φ x Base C G D Func E
97 funcrcl F C Func D C Cat D Cat
98 1 97 syl φ C Cat D Cat
99 98 simpld φ C Cat
100 99 adantr φ x Base C C Cat
101 3 46 84 100 87 catidcl φ x Base C Id C x x Hom C x
102 3 95 96 87 87 46 101 cofu2 φ x Base C x 2 nd G func F x Id C x = 1 st F x 2 nd G 1 st F x x 2 nd F x Id C x
103 3 95 96 87 cofu1 φ x Base C 1 st G func F x = 1 st G 1 st F x
104 103 fveq2d φ x Base C Id E 1 st G func F x = Id E 1 st G 1 st F x
105 94 102 104 3eqtr4d φ x Base C x 2 nd G func F x Id C x = Id E 1 st G func F x
106 86 adantr φ x Base C y Base C z Base C f x Hom C y g y Hom C z 1 st F C Func D 2 nd F
107 simplr φ x Base C y Base C z Base C f x Hom C y g y Hom C z x Base C
108 simprlr φ x Base C y Base C z Base C f x Hom C y g y Hom C z z Base C
109 3 46 37 106 107 108 funcf2 φ x Base C y Base C z Base C f x Hom C y g y Hom C z x 2 nd F z : x Hom C z 1 st F x Hom D 1 st F z
110 eqid comp C = comp C
111 100 adantr φ x Base C y Base C z Base C f x Hom C y g y Hom C z C Cat
112 simprll φ x Base C y Base C z Base C f x Hom C y g y Hom C z y Base C
113 simprrl φ x Base C y Base C z Base C f x Hom C y g y Hom C z f x Hom C y
114 simprrr φ x Base C y Base C z Base C f x Hom C y g y Hom C z g y Hom C z
115 3 46 110 111 107 112 108 113 114 catcocl φ x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z
116 fvco3 x 2 nd F z : x Hom C z 1 st F x Hom D 1 st F z g x y comp C z f x Hom C z 1 st F x 2 nd G 1 st F z x 2 nd F z g x y comp C z f = 1 st F x 2 nd G 1 st F z x 2 nd F z g x y comp C z f
117 109 115 116 syl2anc φ x Base C y Base C z Base C f x Hom C y g y Hom C z 1 st F x 2 nd G 1 st F z x 2 nd F z g x y comp C z f = 1 st F x 2 nd G 1 st F z x 2 nd F z g x y comp C z f
118 eqid comp D = comp D
119 3 46 110 118 106 107 112 108 113 114 funcco φ x Base C y Base C z Base C f x Hom C y g y Hom C z x 2 nd F z g x y comp C z f = y 2 nd F z g 1 st F x 1 st F y comp D 1 st F z x 2 nd F y f
120 119 fveq2d φ x Base C y Base C z Base C f x Hom C y g y Hom C z 1 st F x 2 nd G 1 st F z x 2 nd F z g x y comp C z f = 1 st F x 2 nd G 1 st F z y 2 nd F z g 1 st F x 1 st F y comp D 1 st F z x 2 nd F y f
121 eqid comp E = comp E
122 91 adantr φ x Base C y Base C z Base C f x Hom C y g y Hom C z 1 st G D Func E 2 nd G
123 92 adantr φ x Base C y Base C z Base C f x Hom C y g y Hom C z 1 st F x Base D
124 25 adantr φ x Base C 1 st F : Base C Base D
125 124 adantr φ x Base C y Base C z Base C f x Hom C y g y Hom C z 1 st F : Base C Base D
126 125 112 ffvelrnd φ x Base C y Base C z Base C f x Hom C y g y Hom C z 1 st F y Base D
127 125 108 ffvelrnd φ x Base C y Base C z Base C f x Hom C y g y Hom C z 1 st F z Base D
128 3 46 37 106 107 112 funcf2 φ x Base C y Base C z Base C f x Hom C y g y Hom C z x 2 nd F y : x Hom C y 1 st F x Hom D 1 st F y
129 128 113 ffvelrnd φ x Base C y Base C z Base C f x Hom C y g y Hom C z x 2 nd F y f 1 st F x Hom D 1 st F y
130 3 46 37 106 112 108 funcf2 φ x Base C y Base C z Base C f x Hom C y g y Hom C z y 2 nd F z : y Hom C z 1 st F y Hom D 1 st F z
131 130 114 ffvelrnd φ x Base C y Base C z Base C f x Hom C y g y Hom C z y 2 nd F z g 1 st F y Hom D 1 st F z
132 16 37 118 121 122 123 126 127 129 131 funcco φ x Base C y Base C z Base C f x Hom C y g y Hom C z 1 st F x 2 nd G 1 st F z y 2 nd F z g 1 st F x 1 st F y comp D 1 st F z x 2 nd F y f = 1 st F y 2 nd G 1 st F z y 2 nd F z g 1 st G 1 st F x 1 st G 1 st F y comp E 1 st G 1 st F z 1 st F x 2 nd G 1 st F y x 2 nd F y f
133 117 120 132 3eqtrd φ x Base C y Base C z Base C f x Hom C y g y Hom C z 1 st F x 2 nd G 1 st F z x 2 nd F z g x y comp C z f = 1 st F y 2 nd G 1 st F z y 2 nd F z g 1 st G 1 st F x 1 st G 1 st F y comp E 1 st G 1 st F z 1 st F x 2 nd G 1 st F y x 2 nd F y f
134 95 adantr φ x Base C y Base C z Base C f x Hom C y g y Hom C z F C Func D
135 96 adantr φ x Base C y Base C z Base C f x Hom C y g y Hom C z G D Func E
136 3 134 135 107 108 cofu2nd φ x Base C y Base C z Base C f x Hom C y g y Hom C z x 2 nd G func F z = 1 st F x 2 nd G 1 st F z x 2 nd F z
137 136 fveq1d φ x Base C y Base C z Base C f x Hom C y g y Hom C z x 2 nd G func F z g x y comp C z f = 1 st F x 2 nd G 1 st F z x 2 nd F z g x y comp C z f
138 103 adantr φ x Base C y Base C z Base C f x Hom C y g y Hom C z 1 st G func F x = 1 st G 1 st F x
139 3 134 135 112 cofu1 φ x Base C y Base C z Base C f x Hom C y g y Hom C z 1 st G func F y = 1 st G 1 st F y
140 138 139 opeq12d φ x Base C y Base C z Base C f x Hom C y g y Hom C z 1 st G func F x 1 st G func F y = 1 st G 1 st F x 1 st G 1 st F y
141 3 134 135 108 cofu1 φ x Base C y Base C z Base C f x Hom C y g y Hom C z 1 st G func F z = 1 st G 1 st F z
142 140 141 oveq12d φ x Base C y Base C z Base C f x Hom C y g y Hom C z 1 st G func F x 1 st G func F y comp E 1 st G func F z = 1 st G 1 st F x 1 st G 1 st F y comp E 1 st G 1 st F z
143 3 134 135 112 108 46 114 cofu2 φ x Base C y Base C z Base C f x Hom C y g y Hom C z y 2 nd G func F z g = 1 st F y 2 nd G 1 st F z y 2 nd F z g
144 3 134 135 107 112 46 113 cofu2 φ x Base C y Base C z Base C f x Hom C y g y Hom C z x 2 nd G func F y f = 1 st F x 2 nd G 1 st F y x 2 nd F y f
145 142 143 144 oveq123d φ x Base C y Base C z Base C f x Hom C y g y Hom C z y 2 nd G func F z g 1 st G func F x 1 st G func F y comp E 1 st G func F z x 2 nd G func F y f = 1 st F y 2 nd G 1 st F z y 2 nd F z g 1 st G 1 st F x 1 st G 1 st F y comp E 1 st G 1 st F z 1 st F x 2 nd G 1 st F y x 2 nd F y f
146 133 137 145 3eqtr4d φ x Base C y Base C z Base C f x Hom C y g y Hom C z x 2 nd G func F z g x y comp C z f = y 2 nd G func F z g 1 st G func F x 1 st G func F y comp E 1 st G func F z x 2 nd G func F y f
147 146 anassrs φ x Base C y Base C z Base C f x Hom C y g y Hom C z x 2 nd G func F z g x y comp C z f = y 2 nd G func F z g 1 st G func F x 1 st G func F y comp E 1 st G func F z x 2 nd G func F y f
148 147 ralrimivva φ x Base C y Base C z Base C f x Hom C y g y Hom C z x 2 nd G func F z g x y comp C z f = y 2 nd G func F z g 1 st G func F x 1 st G func F y comp E 1 st G func F z x 2 nd G func F y f
149 148 ralrimivva φ x Base C y Base C z Base C f x Hom C y g y Hom C z x 2 nd G func F z g x y comp C z f = y 2 nd G func F z g 1 st G func F x 1 st G func F y comp E 1 st G func F z x 2 nd G func F y f
150 105 149 jca φ x Base C x 2 nd G func F x Id C x = Id E 1 st G func F x y Base C z Base C f x Hom C y g y Hom C z x 2 nd G func F z g x y comp C z f = y 2 nd G func F z g 1 st G func F x 1 st G func F y comp E 1 st G func F z x 2 nd G func F y f
151 150 ralrimiva φ x Base C x 2 nd G func F x Id C x = Id E 1 st G func F x y Base C z Base C f x Hom C y g y Hom C z x 2 nd G func F z g x y comp C z f = y 2 nd G func F z g 1 st G func F x 1 st G func F y comp E 1 st G func F z x 2 nd G func F y f
152 funcrcl G D Func E D Cat E Cat
153 2 152 syl φ D Cat E Cat
154 153 simprd φ E Cat
155 3 17 46 38 84 90 110 121 99 154 isfunc φ 1 st G func F C Func E 2 nd G func F 1 st G func F : Base C Base E 2 nd G func F z Base C × Base C 1 st G func F 1 st z Hom E 1 st G func F 2 nd z Hom C z x Base C x 2 nd G func F x Id C x = Id E 1 st G func F x y Base C z Base C f x Hom C y g y Hom C z x 2 nd G func F z g x y comp C z f = y 2 nd G func F z g 1 st G func F x 1 st G func F y comp E 1 st G func F z x 2 nd G func F y f
156 29 83 151 155 mpbir3and φ 1 st G func F C Func E 2 nd G func F
157 df-br 1 st G func F C Func E 2 nd G func F 1 st G func F 2 nd G func F C Func E
158 156 157 sylib φ 1 st G func F 2 nd G func F C Func E
159 15 158 eqeltrd φ G func F C Func E