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

Theorem evlfcl 14012
 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 2296 . . . . 5
5 eqid 2296 . . . . 5
6 eqid 2296 . . . . 5 comp comp
7 eqid 2296 . . . . 5 Nat Nat
81, 2, 3, 4, 5, 6, 7evlfval 14007 . . . 4 Nat comp
9 ovex 5899 . . . . . 6
10 fvex 5555 . . . . . 6
119, 10mpt2ex 6214 . . . . 5
129, 10xpex 4817 . . . . . 6
1312, 12mpt2ex 6214 . . . . 5 Nat comp
1411, 13opelvv 4751 . . . 4 Nat comp
158, 14syl6eqel 2384 . . 3
16 1st2nd2 6175 . . 3
1715, 16syl 15 . 2
18 eqid 2296 . . . . 5 c c
19 evlfcl.q . . . . . 6 FuncCat
2019fucbas 13850 . . . . 5
2118, 20, 4xpcbas 13968 . . . 4 c
22 eqid 2296 . . . 4
23 eqid 2296 . . . 4 c c
24 eqid 2296 . . . 4
25 eqid 2296 . . . 4 c c
26 eqid 2296 . . . 4
27 eqid 2296 . . . 4 comp c comp c
2819, 2, 3fuccat 13860 . . . . 5
2918, 28, 2xpccat 13980 . . . 4 c
30 relfunc 13752 . . . . . . . . . . 11
31 simpr 447 . . . . . . . . . . 11
32 1st2ndbr 6185 . . . . . . . . . . 11
3330, 31, 32sylancr 644 . . . . . . . . . 10
344, 22, 33funcf1 13756 . . . . . . . . 9
3534ffvelrnda 5681 . . . . . . . 8
3635ralrimiva 2639 . . . . . . 7
3736ralrimiva 2639 . . . . . 6
38 eqid 2296 . . . . . . 7
3938fmpt2 6207 . . . . . 6
4037, 39sylib 188 . . . . 5
4111, 13op1std 6146 . . . . . . 7 Nat comp
428, 41syl 15 . . . . . 6
4342feq1d 5395 . . . . 5
4440, 43mpbird 223 . . . 4
45 eqid 2296 . . . . . 6 Nat comp Nat comp
46 fvex 5555 . . . . . . 7
47 fvex 5555 . . . . . . . 8
48 ovex 5899 . . . . . . . . 9 Nat
49 ovex 5899 . . . . . . . . 9
5048, 49mpt2ex 6214 . . . . . . . 8 Nat comp
5147, 50csbex 3105 . . . . . . 7 Nat comp
5246, 51csbex 3105 . . . . . 6 Nat comp
5345, 52fnmpt2i 6209 . . . . 5 Nat comp
5411, 13op2ndd 6147 . . . . . . 7 Nat comp Nat comp
558, 54syl 15 . . . . . 6 Nat comp
5655fneq1d 5351 . . . . 5 Nat comp
5753, 56mpbiri 224 . . . 4
583ad2antrr 706 . . . . . . . . . . . . . . . 16
5958adantr 451 . . . . . . . . . . . . . . 15 Nat
60 simplrl 736 . . . . . . . . . . . . . . . . . . 19
6130, 60, 32sylancr 644 . . . . . . . . . . . . . . . . . 18
624, 22, 61funcf1 13756 . . . . . . . . . . . . . . . . 17
6362adantr 451 . . . . . . . . . . . . . . . 16 Nat
64 simplrr 737 . . . . . . . . . . . . . . . . 17
6564adantr 451 . . . . . . . . . . . . . . . 16 Nat
6663, 65ffvelrnd 5682 . . . . . . . . . . . . . . 15 Nat
67 simprr 733 . . . . . . . . . . . . . . . . 17
6867adantr 451 . . . . . . . . . . . . . . . 16 Nat
6963, 68ffvelrnd 5682 . . . . . . . . . . . . . . 15 Nat
70 simprl 732 . . . . . . . . . . . . . . . . . . 19
71 1st2ndbr 6185 . . . . . . . . . . . . . . . . . . 19
7230, 70, 71sylancr 644 . . . . . . . . . . . . . . . . . 18
734, 22, 72funcf1 13756 . . . . . . . . . . . . . . . . 17
7473adantr 451 . . . . . . . . . . . . . . . 16 Nat
7574, 68ffvelrnd 5682 . . . . . . . . . . . . . . 15 Nat
764, 5, 24, 61, 64, 67funcf2 13758 . . . . . . . . . . . . . . . . 17
7776adantr 451 . . . . . . . . . . . . . . . 16 Nat
78 simprr 733 . . . . . . . . . . . . . . . 16 Nat
7977, 78ffvelrnd 5682 . . . . . . . . . . . . . . 15 Nat
80 simprl 732 . . . . . . . . . . . . . . . . 17 Nat Nat
817, 80nat1st2nd 13841 . . . . . . . . . . . . . . . 16 Nat Nat
827, 81, 4, 24, 68natcl 13843 . . . . . . . . . . . . . . 15 Nat
8322, 24, 6, 59, 66, 69, 75, 79, 82catcocl 13603 . . . . . . . . . . . . . 14 Nat comp
8483ralrimivva 2648 . . . . . . . . . . . . 13 Nat comp
85 eqid 2296 . . . . . . . . . . . . . 14 Nat comp Nat comp
8685fmpt2 6207 . . . . . . . . . . . . 13 Nat comp Nat comp Nat
8784, 86sylib 188 . . . . . . . . . . . 12 Nat comp Nat
882ad2antrr 706 . . . . . . . . . . . . . 14
89 eqid 2296 . . . . . . . . . . . . . 14
901, 88, 58, 4, 5, 6, 7, 60, 70, 64, 67, 89evlf2 14008 . . . . . . . . . . . . 13 Nat comp
9190feq1d 5395 . . . . . . . . . . . 12 Nat Nat comp Nat
9287, 91mpbird 223 . . . . . . . . . . 11 Nat
9319, 7fuchom 13851 . . . . . . . . . . . . 13 Nat
9418, 20, 4, 93, 5, 60, 64, 70, 67, 23xpchom2 13976 . . . . . . . . . . . 12 c Nat
951, 88, 58, 4, 60, 64evlf1 14010 . . . . . . . . . . . . 13
961, 88, 58, 4, 70, 67evlf1 14010 . . . . . . . . . . . . 13
9795, 96oveq12d 5892 . . . . . . . . . . . 12
9894, 97feq23d 5402 . . . . . . . . . . 11 c Nat
9992, 98mpbird 223 . . . . . . . . . 10 c
10099ralrimivva 2648 . . . . . . . . 9 c
101100ralrimivva 2648 . . . . . . . 8 c
102 oveq2 5882 . . . . . . . . . . . . 13
103102feq1d 5395 . . . . . . . . . . . 12 c c
104 oveq2 5882 . . . . . . . . . . . . 13 c c
105 fveq2 5541 . . . . . . . . . . . . . . 15
106 df-ov 5877 . . . . . . . . . . . . . . 15
107105, 106syl6eqr 2346 . . . . . . . . . . . . . 14
108107oveq2d 5890 . . . . . . . . . . . . 13
109104, 108feq23d 5402 . . . . . . . . . . . 12 c c
110103, 109bitrd 244 . . . . . . . . . . 11 c c
111110ralxp 4843 . . . . . . . . . 10 c c
112 oveq1 5881 . . . . . . . . . . . . 13
113112feq1d 5395 . . . . . . . . . . . 12 c c
114 oveq1 5881 . . . . . . . . . . . . 13 c c
115 fveq2 5541 . . . . . . . . . . . . . . 15
116 df-ov 5877 . . . . . . . . . . . . . . 15
117115, 116syl6eqr 2346 . . . . . . . . . . . . . 14
118117oveq1d 5889 . . . . . . . . . . . . 13
119114, 118feq23d 5402 . . . . . . . . . . . 12 c c
120113, 119bitrd 244 . . . . . . . . . . 11 c c
1211202ralbidv 2598 . . . . . . . . . 10 c c
122111, 121syl5bb 248 . . . . . . . . 9 c c
123122ralxp 4843 . . . . . . . 8 c c
124101, 123sylibr 203 . . . . . . 7 c
125124r19.21bi 2654 . . . . . 6 c
126125r19.21bi 2654 . . . . 5 c
127126anasss 628 . . . 4 c
12828adantr 451 . . . . . . . . . . 11
1292adantr 451 . . . . . . . . . . 11
130 eqid 2296 . . . . . . . . . . 11
131 eqid 2296 . . . . . . . . . . 11
13231adantrr 697 . . . . . . . . . . 11
133 simprr 733 . . . . . . . . . . 11
13418, 128, 129, 20, 4, 130, 131, 25, 132, 133xpcid 13979 . . . . . . . . . 10 c
135134fveq2d 5545 . . . . . . . . 9 c
136 df-ov 5877 . . . . . . . . 9
137135, 136syl6eqr 2346 . . . . . . . 8 c
1383adantr 451 . . . . . . . . 9
139 eqid 2296 . . . . . . . . 9
14020, 93, 130, 128, 132catidcl 13600 . . . . . . . . 9 Nat
1414, 5, 131, 129, 133catidcl 13600 . . . . . . . . 9
1421, 129, 138, 4, 5, 6, 7, 132, 132, 133, 133, 139, 140, 141evlf2val 14009 . . . . . . . 8 comp
143 simprl 732 . . . . . . . . . . . . 13
14430, 143, 32sylancr 644 . . . . . . . . . . . 12
1454, 22, 144funcf1 13756 . . . . . . . . . . 11
146145, 133ffvelrnd 5682 . . . . . . . . . 10
14722, 24, 26, 138, 146catidcl 13600 . . . . . . . . . 10
14822, 24, 26, 138, 146, 6, 146, 147catlid 13601 . . . . . . . . 9 comp
14919, 130, 26, 132fucid 13861 . . . . . . . . . . . 12
150149fveq1d 5543 . . . . . . . . . . 11
151 fvco3 5612 . . . . . . . . . . . 12
152145, 133, 151syl2anc 642 . . . . . . . . . . 11
153150, 152eqtrd 2328 . . . . . . . . . 10
1544, 131, 26, 144, 133funcid 13760 . . . . . . . . . 10
155153, 154oveq12d 5892 . . . . . . . . 9 comp comp
1561, 129, 138, 4, 132, 133evlf1 14010 . . . . . . . . . 10
157156fveq2d 5545 . . . . . . . . 9
158148, 155, 1573eqtr4d 2338 . . . . . . . 8 comp
159137, 142, 1583eqtrd 2332 . . . . . . 7 c
160159ralrimivva 2648 . . . . . 6 c
161 id 19 . . . . . . . . . 10
162161, 161oveq12d 5892 . . . . . . . . 9
163 fveq2 5541 . . . . . . . . 9 c c
164162, 163fveq12d 5547 . . . . . . . 8 c c
165117fveq2d 5545 . . . . . . . 8
166164, 165eqeq12d 2310 . . . . . . 7 c c
167166ralxp 4843 . . . . . 6 c c
168160, 167sylibr 203 . . . . 5 c
169168r19.21bi 2654 . . . 4 c
17023ad2ant1 976 . . . . . 6 c c
17133ad2ant1 976 . . . . . 6 c c
172 simp21 988 . . . . . . . . 9 c c
173 1st2nd2 6175 . . . . . . . . 9
174172, 173syl 15 . . . . . . . 8 c c
175174, 172eqeltrrd 2371 . . . . . . 7 c c
176 opelxp 4735 . . . . . . 7
177175, 176sylib 188 . . . . . 6 c c
178 simp22 989 . . . . . . . . 9 c c
179 1st2nd2 6175 . . . . . . . . 9
180178, 179syl 15 . . . . . . . 8 c c
181180, 178eqeltrrd 2371 . . . . . . 7 c c
182 opelxp 4735 . . . . . . 7
183181, 182sylib 188 . . . . . 6 c c
184 simp23 990 . . . . . . . . 9 c c
185 1st2nd2 6175 . . . . . . . . 9
186184, 185syl 15 . . . . . . . 8 c c
187186, 184eqeltrrd 2371 . . . . . . 7 c c
188 opelxp 4735 . . . . . . 7
189187, 188sylib 188 . . . . . 6 c c
190 simp3l 983 . . . . . . . . . 10 c c c
19118, 21, 93, 5, 23, 172, 178xpchom 13970 . . . . . . . . . 10 c c c Nat
192190, 191eleqtrd 2372 . . . . . . . . 9 c c Nat
193 1st2nd2 6175 . . . . . . . . 9 Nat
194192, 193syl 15 . . . . . . . 8 c c
195194, 192eqeltrrd 2371 . . . . . . 7 c c Nat
196 opelxp 4735 . . . . . . 7 Nat Nat
197195, 196sylib 188 . . . . . 6 c c Nat
198 simp3r 984 . . . . . . . . . 10 c c c
19918, 21, 93, 5, 23, 178, 184xpchom 13970 . . . . . . . . . 10 c c c Nat
200198, 199eleqtrd 2372 . . . . . . . . 9 c c Nat
201 1st2nd2 6175 . . . . . . . . 9 Nat
202200, 201syl 15 . . . . . . . 8 c c
203202, 200eqeltrrd 2371 . . . . . . 7 c c Nat
204 opelxp 4735 . . . . . . 7 Nat Nat
205203, 204sylib 188 . . . . . 6 c c Nat
2061, 19, 170, 171, 7, 177, 183, 189, 197, 205evlfcllem 14011 . . . . 5 c c comp c comp
207174, 186oveq12d 5892 . . . . . 6