Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  evlfcl Structured version   Unicode version

Theorem evlfcl 14321
 Description: The evaluation functor is a bifunctor (a two-argument functor) with the first parameter taking values in the set of functors , and the second parameter in . (Contributed by Mario Carneiro, 12-Jan-2017.)
Hypotheses
Ref Expression
evlfcl.e evalF
evlfcl.q FuncCat
evlfcl.c
evlfcl.d
Assertion
Ref Expression
evlfcl c

Proof of Theorem evlfcl
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 evlfcl.e . . . . 5 evalF
2 evlfcl.c . . . . 5
3 evlfcl.d . . . . 5
4 eqid 2438 . . . . 5
5 eqid 2438 . . . . 5
6 eqid 2438 . . . . 5 comp comp
7 eqid 2438 . . . . 5 Nat Nat
81, 2, 3, 4, 5, 6, 7evlfval 14316 . . . 4 Nat comp
9 ovex 6108 . . . . . 6
10 fvex 5744 . . . . . 6
119, 10mpt2ex 6427 . . . . 5
129, 10xpex 4992 . . . . . 6
1312, 12mpt2ex 6427 . . . . 5 Nat comp
1411, 13opelvv 4926 . . . 4 Nat comp
158, 14syl6eqel 2526 . . 3
16 1st2nd2 6388 . . 3
1715, 16syl 16 . 2
18 eqid 2438 . . . . 5 c c
19 evlfcl.q . . . . . 6 FuncCat
2019fucbas 14159 . . . . 5
2118, 20, 4xpcbas 14277 . . . 4 c
22 eqid 2438 . . . 4
23 eqid 2438 . . . 4 c c
24 eqid 2438 . . . 4
25 eqid 2438 . . . 4 c c
26 eqid 2438 . . . 4
27 eqid 2438 . . . 4 comp c comp c
2819, 2, 3fuccat 14169 . . . . 5
2918, 28, 2xpccat 14289 . . . 4 c
30 relfunc 14061 . . . . . . . . . . 11
31 simpr 449 . . . . . . . . . . 11
32 1st2ndbr 6398 . . . . . . . . . . 11
3330, 31, 32sylancr 646 . . . . . . . . . 10
344, 22, 33funcf1 14065 . . . . . . . . 9
3534ffvelrnda 5872 . . . . . . . 8
3635ralrimiva 2791 . . . . . . 7
3736ralrimiva 2791 . . . . . 6
38 eqid 2438 . . . . . . 7
3938fmpt2 6420 . . . . . 6
4037, 39sylib 190 . . . . 5
4111, 13op1std 6359 . . . . . . 7 Nat comp
428, 41syl 16 . . . . . 6
4342feq1d 5582 . . . . 5
4440, 43mpbird 225 . . . 4
45 eqid 2438 . . . . . 6 Nat comp Nat comp
46 fvex 5744 . . . . . . 7
47 fvex 5744 . . . . . . . 8
48 ovex 6108 . . . . . . . . 9 Nat
49 ovex 6108 . . . . . . . . 9
5048, 49mpt2ex 6427 . . . . . . . 8 Nat comp
5147, 50csbex 3264 . . . . . . 7 Nat comp
5246, 51csbex 3264 . . . . . 6 Nat comp
5345, 52fnmpt2i 6422 . . . . 5 Nat comp
5411, 13op2ndd 6360 . . . . . . 7 Nat comp Nat comp
558, 54syl 16 . . . . . 6 Nat comp
5655fneq1d 5538 . . . . 5 Nat comp
5753, 56mpbiri 226 . . . 4
583ad2antrr 708 . . . . . . . . . . . . . . . 16
5958adantr 453 . . . . . . . . . . . . . . 15 Nat
60 simplrl 738 . . . . . . . . . . . . . . . . . . 19
6130, 60, 32sylancr 646 . . . . . . . . . . . . . . . . . 18
624, 22, 61funcf1 14065 . . . . . . . . . . . . . . . . 17
6362adantr 453 . . . . . . . . . . . . . . . 16 Nat
64 simplrr 739 . . . . . . . . . . . . . . . . 17
6564adantr 453 . . . . . . . . . . . . . . . 16 Nat
6663, 65ffvelrnd 5873 . . . . . . . . . . . . . . 15 Nat
67 simplrr 739 . . . . . . . . . . . . . . . 16 Nat
6863, 67ffvelrnd 5873 . . . . . . . . . . . . . . 15 Nat
69 simprl 734 . . . . . . . . . . . . . . . . . . 19
70 1st2ndbr 6398 . . . . . . . . . . . . . . . . . . 19
7130, 69, 70sylancr 646 . . . . . . . . . . . . . . . . . 18
724, 22, 71funcf1 14065 . . . . . . . . . . . . . . . . 17
7372adantr 453 . . . . . . . . . . . . . . . 16 Nat
7473, 67ffvelrnd 5873 . . . . . . . . . . . . . . 15 Nat
75 simprr 735 . . . . . . . . . . . . . . . . . 18
764, 5, 24, 61, 64, 75funcf2 14067 . . . . . . . . . . . . . . . . 17
7776adantr 453 . . . . . . . . . . . . . . . 16 Nat
78 simprr 735 . . . . . . . . . . . . . . . 16 Nat
7977, 78ffvelrnd 5873 . . . . . . . . . . . . . . 15 Nat
80 simprl 734 . . . . . . . . . . . . . . . . 17 Nat Nat
817, 80nat1st2nd 14150 . . . . . . . . . . . . . . . 16 Nat Nat
827, 81, 4, 24, 67natcl 14152 . . . . . . . . . . . . . . 15 Nat
8322, 24, 6, 59, 66, 68, 74, 79, 82catcocl 13912 . . . . . . . . . . . . . 14 Nat comp
8483ralrimivva 2800 . . . . . . . . . . . . 13 Nat comp
85 eqid 2438 . . . . . . . . . . . . . 14 Nat comp Nat comp
8685fmpt2 6420 . . . . . . . . . . . . 13 Nat comp Nat comp Nat
8784, 86sylib 190 . . . . . . . . . . . 12 Nat comp Nat
882ad2antrr 708 . . . . . . . . . . . . . 14
89 eqid 2438 . . . . . . . . . . . . . 14
901, 88, 58, 4, 5, 6, 7, 60, 69, 64, 75, 89evlf2 14317 . . . . . . . . . . . . 13 Nat comp
9190feq1d 5582 . . . . . . . . . . . 12 Nat Nat comp Nat
9287, 91mpbird 225 . . . . . . . . . . 11 Nat
9319, 7fuchom 14160 . . . . . . . . . . . . 13 Nat
9418, 20, 4, 93, 5, 60, 64, 69, 75, 23xpchom2 14285 . . . . . . . . . . . 12 c Nat
951, 88, 58, 4, 60, 64evlf1 14319 . . . . . . . . . . . . 13
961, 88, 58, 4, 69, 75evlf1 14319 . . . . . . . . . . . . 13
9795, 96oveq12d 6101 . . . . . . . . . . . 12
9894, 97feq23d 5590 . . . . . . . . . . 11 c Nat
9992, 98mpbird 225 . . . . . . . . . 10 c
10099ralrimivva 2800 . . . . . . . . 9 c
101100ralrimivva 2800 . . . . . . . 8 c
102 oveq2 6091 . . . . . . . . . . . 12
103 oveq2 6091 . . . . . . . . . . . 12 c c
104 fveq2 5730 . . . . . . . . . . . . . 14
105 df-ov 6086 . . . . . . . . . . . . . 14
106104, 105syl6eqr 2488 . . . . . . . . . . . . 13
107106oveq2d 6099 . . . . . . . . . . . 12
108102, 103, 107feq123d 5585 . . . . . . . . . . 11 c c
109108ralxp 5018 . . . . . . . . . 10 c c
110 oveq1 6090 . . . . . . . . . . . 12
111 oveq1 6090 . . . . . . . . . . . 12 c c
112 fveq2 5730 . . . . . . . . . . . . . 14
113 df-ov 6086 . . . . . . . . . . . . . 14
114112, 113syl6eqr 2488 . . . . . . . . . . . . 13
115114oveq1d 6098 . . . . . . . . . . . 12
116110, 111, 115feq123d 5585 . . . . . . . . . . 11 c c
1171162ralbidv 2749 . . . . . . . . . 10 c c
118109, 117syl5bb 250 . . . . . . . . 9 c c
119118ralxp 5018 . . . . . . . 8 c c
120101, 119sylibr 205 . . . . . . 7 c
121120r19.21bi 2806 . . . . . 6 c
122121r19.21bi 2806 . . . . 5 c
123122anasss 630 . . . 4 c
12428adantr 453 . . . . . . . . . . 11
1252adantr 453 . . . . . . . . . . 11
126 eqid 2438 . . . . . . . . . . 11
127 eqid 2438 . . . . . . . . . . 11
128 simprl 734 . . . . . . . . . . 11
129 simprr 735 . . . . . . . . . . 11
13018, 124, 125, 20, 4, 126, 127, 25, 128, 129xpcid 14288 . . . . . . . . . 10 c
131130fveq2d 5734 . . . . . . . . 9 c
132 df-ov 6086 . . . . . . . . 9
133131, 132syl6eqr 2488 . . . . . . . 8 c
1343adantr 453 . . . . . . . . 9
135 eqid 2438 . . . . . . . . 9
13620, 93, 126, 124, 128catidcl 13909 . . . . . . . . 9 Nat
1374, 5, 127, 125, 129catidcl 13909 . . . . . . . . 9
1381, 125, 134, 4, 5, 6, 7, 128, 128, 129, 129, 135, 136, 137evlf2val 14318 . . . . . . . 8 comp
13930, 128, 32sylancr 646 . . . . . . . . . . . 12
1404, 22, 139funcf1 14065 . . . . . . . . . . 11
141140, 129ffvelrnd 5873 . . . . . . . . . 10
14222, 24, 26, 134, 141catidcl 13909 . . . . . . . . . 10
14322, 24, 26, 134, 141, 6, 141, 142catlid 13910 . . . . . . . . 9 comp
14419, 126, 26, 128fucid 14170 . . . . . . . . . . . 12
145144fveq1d 5732 . . . . . . . . . . 11
146 fvco3 5802 . . . . . . . . . . . 12
147140, 129, 146syl2anc 644 . . . . . . . . . . 11
148145, 147eqtrd 2470 . . . . . . . . . 10
1494, 127, 26, 139, 129funcid 14069 . . . . . . . . . 10
150148, 149oveq12d 6101 . . . . . . . . 9 comp comp
1511, 125, 134, 4, 128, 129evlf1 14319 . . . . . . . . . 10
152151fveq2d 5734 . . . . . . . . 9
153143, 150, 1523eqtr4d 2480 . . . . . . . 8 comp
154133, 138, 1533eqtrd 2474 . . . . . . 7 c
155154ralrimivva 2800 . . . . . 6 c
156 id 21 . . . . . . . . . 10
157156, 156oveq12d 6101 . . . . . . . . 9
158 fveq2 5730 . . . . . . . . 9 c c
159157, 158fveq12d 5736 . . . . . . . 8 c c
160114fveq2d 5734 . . . . . . . 8
161159, 160eqeq12d 2452 . . . . . . 7 c c
162161ralxp 5018 . . . . . 6 c c
163155, 162sylibr 205 . . . . 5 c
164163r19.21bi 2806 . . . 4 c
16523ad2ant1 979 . . . . . 6 c c
16633ad2ant1 979 . . . . . 6 c c
167 simp21 991 . . . . . . . . 9 c c
168 1st2nd2 6388 . . . . . . . . 9
169167, 168syl 16 . . . . . . . 8 c c
170169, 167eqeltrrd 2513 . . . . . . 7 c c
171 opelxp 4910 . . . . . . 7
172170, 171sylib 190 . . . . . 6 c c
173 simp22 992 . . . . . . . . 9 c c
174 1st2nd2 6388 . . . . . . . . 9
175173, 174syl 16 . . . . . . . 8 c c
176175, 173eqeltrrd 2513 . . . . . . 7 c c
177 opelxp 4910 . . . . . . 7
178176, 177sylib 190 . . . . . 6 c c
179 simp23 993 . . . . . . . . 9 c c
180 1st2nd2 6388 . . . . . . . . 9
181179, 180syl 16 . . . . . . . 8 c c
182181, 179eqeltrrd 2513 . . . . . . 7 c c
183 opelxp 4910 . . . . . . 7
184182, 183sylib 190 . . . . . 6 c c
185 simp3l 986 . . . . . . . . . 10 c c c
18618, 21, 93, 5, 23, 167, 173xpchom 14279 . . . . . . . . . 10 c c c Nat
187185, 186eleqtrd 2514 . . . . . . . . 9 c c Nat
188 1st2nd2 6388 . . . . . . . . 9 Nat
189187, 188syl 16 . . . . . . . 8 c c
190189, 187eqeltrrd 2513 . . . . . . 7 c c Nat
191 opelxp 4910 . . . . . . 7 Nat Nat
192190, 191sylib 190 . . . . . 6 c c Nat
193 simp3r 987 . . . . . . . . . 10 c c c
19418, 21, 93, 5, 23, 173, 179xpchom 14279 . . . . . . . . . 10 c c c Nat
195193, 194eleqtrd 2514 . . . . . . . . 9 c c Nat
196 1st2nd2 6388 . . . . . . . . 9 Nat
197195, 196syl 16 . . . . . . . 8 c c
198197, 195eqeltrrd 2513 . . . . . . 7 c c Nat
199 opelxp 4910 . . . . . . 7 Nat Nat
200198, 199sylib 190 . . . . . 6 c c Nat
2011, 19, 165, 166, 7, 172, 178, 184, 192, 200evlfcllem 14320 . . . . 5 c c comp c comp
202169, 181oveq12d 6101 . . . . . 6 c c
203169, 175opeq12d 3994 . . . . . . . 8 c c
204203, 181oveq12d 6101 . . . . . . 7 c c comp c comp c
205204, 197, 189oveq123d 6104 . . . . . 6 c c comp c comp c
206202, 205fveq12d 5736 . . . . 5