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

Theorem yonedainv 14333
 Description: The Yoneda Lemma with explicit inverse. (Contributed by Mario Carneiro, 29-Jan-2017.)
Hypotheses
Ref Expression
yoneda.y Yon
yoneda.b
yoneda.1
yoneda.o oppCat
yoneda.s
yoneda.t
yoneda.q FuncCat
yoneda.h HomF
yoneda.r c FuncCat
yoneda.e evalF
yoneda.z func tpos func F ⟨,⟩F F
yoneda.c
yoneda.w
yoneda.u f
yoneda.v f
yoneda.m Nat
yonedainv.i Inv
yonedainv.n
Assertion
Ref Expression
yonedainv
Distinct variable groups:   ,,,,,   ,,,,,,   ,,,,,   ,,,,,,   ,   ,,,,,,   ,,,,,,   ,,,   ,,,,,   ,,,,   ,,,,,,   ,   ,,,,,,   ,,,,,,
Allowed substitution hints:   ()   (,,,,)   (,)   (,,,,,)   ()   ()   (,,,,,)   (,,,,,)   (,,)   (,,,,)   (,,,,,)   (,,,,,)

Proof of Theorem yonedainv
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 yoneda.r . . 3 c FuncCat
2 eqid 2404 . . . 4 c c
3 yoneda.q . . . . 5 FuncCat
43fucbas 14112 . . . 4
5 yoneda.o . . . . 5 oppCat
6 yoneda.b . . . . 5
75, 6oppcbas 13899 . . . 4
82, 4, 7xpcbas 14230 . . 3 c
9 eqid 2404 . . 3 c Nat c Nat
10 yoneda.y . . . . 5 Yon
11 yoneda.1 . . . . 5
12 yoneda.s . . . . 5
13 yoneda.t . . . . 5
14 yoneda.h . . . . 5 HomF
15 yoneda.e . . . . 5 evalF
16 yoneda.z . . . . 5 func tpos func F ⟨,⟩F F
17 yoneda.c . . . . 5
18 yoneda.w . . . . 5
19 yoneda.u . . . . 5 f
20 yoneda.v . . . . 5 f
2110, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 17, 18, 19, 20yonedalem1 14324 . . . 4 c c
2221simpld 446 . . 3 c
2321simprd 450 . . 3 c
24 yonedainv.i . . 3 Inv
25 eqid 2404 . . 3 Inv Inv
26 yoneda.m . . . 4 Nat
2710, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 17, 18, 19, 20, 26yonedalem3 14332 . . 3 c Nat
2817adantr 452 . . . . . . . . . . 11
2918adantr 452 . . . . . . . . . . 11
3019adantr 452 . . . . . . . . . . 11 f
3120adantr 452 . . . . . . . . . . 11 f
32 simprl 733 . . . . . . . . . . 11
33 simprr 734 . . . . . . . . . . 11
3410, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 28, 29, 30, 31, 32, 33, 26yonedalem3a 14326 . . . . . . . . . 10 Nat
3534simprd 450 . . . . . . . . 9
3628adantr 452 . . . . . . . . . . . 12
3729adantr 452 . . . . . . . . . . . 12
3830adantr 452 . . . . . . . . . . . 12 f
3931adantr 452 . . . . . . . . . . . 12 f
40 simplrl 737 . . . . . . . . . . . 12
41 simplrr 738 . . . . . . . . . . . 12
42 yonedainv.n . . . . . . . . . . . 12
43 simpr 448 . . . . . . . . . . . 12
4410, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 36, 37, 38, 39, 40, 41, 42, 43yonedalem4c 14329 . . . . . . . . . . 11 Nat
45 eqid 2404 . . . . . . . . . . 11
4644, 45fmptd 5852 . . . . . . . . . 10 Nat
47 fvex 5701 . . . . . . . . . . . . . . . 16
486, 47eqeltri 2474 . . . . . . . . . . . . . . 15
4948mptex 5925 . . . . . . . . . . . . . 14
50 eqid 2404 . . . . . . . . . . . . . 14
5149, 50fnmpti 5532 . . . . . . . . . . . . 13
52 simpl 444 . . . . . . . . . . . . . . . . . . 19
5352fveq2d 5691 . . . . . . . . . . . . . . . . . 18
54 simpr 448 . . . . . . . . . . . . . . . . . 18
5553, 54fveq12d 5693 . . . . . . . . . . . . . . . . 17
56 simplr 732 . . . . . . . . . . . . . . . . . . . 20
5756oveq2d 6056 . . . . . . . . . . . . . . . . . . 19
58 simpll 731 . . . . . . . . . . . . . . . . . . . . . . 23
5958fveq2d 5691 . . . . . . . . . . . . . . . . . . . . . 22
60 eqidd 2405 . . . . . . . . . . . . . . . . . . . . . 22
6159, 56, 60oveq123d 6061 . . . . . . . . . . . . . . . . . . . . 21
6261fveq1d 5689 . . . . . . . . . . . . . . . . . . . 20
6362fveq1d 5689 . . . . . . . . . . . . . . . . . . 19
6457, 63mpteq12dv 4247 . . . . . . . . . . . . . . . . . 18
6564mpteq2dva 4255 . . . . . . . . . . . . . . . . 17
6655, 65mpteq12dv 4247 . . . . . . . . . . . . . . . 16
67 fvex 5701 . . . . . . . . . . . . . . . . 17
6867mptex 5925 . . . . . . . . . . . . . . . 16
6966, 42, 68ovmpt2a 6163 . . . . . . . . . . . . . . 15
7069adantl 453 . . . . . . . . . . . . . 14
7170fneq1d 5495 . . . . . . . . . . . . 13
7251, 71mpbiri 225 . . . . . . . . . . . 12
73 dffn5 5731 . . . . . . . . . . . 12
7472, 73sylib 189 . . . . . . . . . . 11
755oppccat 13903 . . . . . . . . . . . . . 14
7617, 75syl 16 . . . . . . . . . . . . 13
7776adantr 452 . . . . . . . . . . . 12
7820unssbd 3485 . . . . . . . . . . . . . . 15
7918, 78ssexd 4310 . . . . . . . . . . . . . 14
8012setccat 14195 . . . . . . . . . . . . . 14
8179, 80syl 16 . . . . . . . . . . . . 13
8281adantr 452 . . . . . . . . . . . 12
8315, 77, 82, 7, 32, 33evlf1 14272 . . . . . . . . . . 11
8410, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 28, 29, 30, 31, 32, 33yonedalem21 14325 . . . . . . . . . . 11 Nat
8574, 83, 84feq123d 5542 . . . . . . . . . 10 Nat
8646, 85mpbird 224 . . . . . . . . 9
87 fcompt 5863 . . . . . . . . . . 11
8835, 86, 87syl2anc 643 . . . . . . . . . 10
8983eleq2d 2471 . . . . . . . . . . . . . 14
9089biimpa 471 . . . . . . . . . . . . 13
9128adantr 452 . . . . . . . . . . . . . . . . 17
9229adantr 452 . . . . . . . . . . . . . . . . 17
9330adantr 452 . . . . . . . . . . . . . . . . 17 f
9431adantr 452 . . . . . . . . . . . . . . . . 17 f
95 simplrl 737 . . . . . . . . . . . . . . . . 17
96 simplrr 738 . . . . . . . . . . . . . . . . 17
9710, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 91, 92, 93, 94, 95, 96, 26yonedalem3a 14326 . . . . . . . . . . . . . . . 16 Nat
9897simpld 446 . . . . . . . . . . . . . . 15 Nat
9998fveq1d 5689 . . . . . . . . . . . . . 14 Nat
100 fvex 5701 . . . . . . . . . . . . . . . . . 18
101100a1i 11 . . . . . . . . . . . . . . . . 17
102101, 74, 44fmpt2d 5857 . . . . . . . . . . . . . . . 16 Nat
103102ffvelrnda 5829 . . . . . . . . . . . . . . 15 Nat
104 fveq1 5686 . . . . . . . . . . . . . . . . 17
105104fveq1d 5689 . . . . . . . . . . . . . . . 16
106 eqid 2404 . . . . . . . . . . . . . . . 16 Nat Nat
107 fvex 5701 . . . . . . . . . . . . . . . 16
108105, 106, 107fvmpt 5765 . . . . . . . . . . . . . . 15 Nat Nat
109103, 108syl 16 . . . . . . . . . . . . . 14 Nat
110 simpr 448 . . . . . . . . . . . . . . . 16
111 eqid 2404 . . . . . . . . . . . . . . . . 17
1126, 111, 11, 91, 96catidcl 13862 . . . . . . . . . . . . . . . 16
11310, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 91, 92, 93, 94, 95, 96, 42, 110, 96, 112yonedalem4b 14328 . . . . . . . . . . . . . . 15
114 eqid 2404 . . . . . . . . . . . . . . . . . 18
115 eqid 2404 . . . . . . . . . . . . . . . . . 18
116 relfunc 14014 . . . . . . . . . . . . . . . . . . 19
117 1st2ndbr 6355 . . . . . . . . . . . . . . . . . . 19
118116, 95, 117sylancr 645 . . . . . . . . . . . . . . . . . 18
1197, 114, 115, 118, 96funcid 14022 . . . . . . . . . . . . . . . . 17
1205, 11oppcid 13902 . . . . . . . . . . . . . . . . . . . 20
12191, 120syl 16 . . . . . . . . . . . . . . . . . . 19
122121fveq1d 5689 . . . . . . . . . . . . . . . . . 18
123122fveq2d 5691 . . . . . . . . . . . . . . . . 17
12479ad2antrr 707 . . . . . . . . . . . . . . . . . 18
125 eqid 2404 . . . . . . . . . . . . . . . . . . . . 21
1267, 125, 118funcf1 14018 . . . . . . . . . . . . . . . . . . . 20
127 eqidd 2405 . . . . . . . . . . . . . . . . . . . . 21
12812, 124setcbas 14188 . . . . . . . . . . . . . . . . . . . . 21
129127, 128feq23d 5547 . . . . . . . . . . . . . . . . . . . 20
130126, 129mpbird 224 . . . . . . . . . . . . . . . . . . 19
131130, 96ffvelrnd 5830 . . . . . . . . . . . . . . . . . 18
13212, 115, 124, 131setcid 14196 . . . . . . . . . . . . . . . . 17
133119, 123, 1323eqtr3d 2444 . . . . . . . . . . . . . . . 16
134133fveq1d 5689 . . . . . . . . . . . . . . 15
135 fvresi 5883 . . . . . . . . . . . . . . . 16
136135adantl 453 . . . . . . . . . . . . . . 15
137113, 134, 1363eqtrd 2440 . . . . . . . . . . . . . 14
13899, 109, 1373eqtrd 2440 . . . . . . . . . . . . 13
13990, 138syldan 457 . . . . . . . . . . . 12
140139mpteq2dva 4255 . . . . . . . . . . 11
141 mptresid 5154 . . . . . . . . . . 11
142140, 141syl6eq 2452 . . . . . . . . . 10
14388, 142eqtrd 2436 . . . . . . . . 9
144 fcompt 5863 . . . . . . . . . . 11
14586, 35, 144syl2anc 643 . . . . . . . . . 10
146 eqid 2404 . . . . . . . . . . . . . 14 Nat Nat
14728adantr 452 . . . . . . . . . . . . . . . 16
14829adantr 452 . . . . . . . . . . . . . . . 16
14930adantr 452 . . . . . . . . . . . . . . . 16 f
15031adantr 452 . . . . . . . . . . . . . . . 16 f
151 simplrl 737 . . . . . . . . . . . . . . . 16
152 simplrr 738 . . . . . . . . . . . . . . . 16
153 eqidd 2405 . . . . . . . . . . . . . . . . . . 19
154153, 83feq23d 5547 . . . . . . . . . . . . . . . . . 18
15535, 154mpbid 202 . . . . . . . . . . . . . . . . 17
156155ffvelrnda 5829 . . . . . . . . . . . . . . . 16
15710, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 147, 148, 149, 150, 151, 152, 42, 156yonedalem4c 14329 . . . . . . . . . . . . . . 15 Nat
158146, 157nat1st2nd 14103 . . . . . . . . . . . . . 14 Nat
159146, 158, 7natfn 14106 . . . . . . . . . . . . 13
16084eleq2d 2471 . . . . . . . . . . . . . . . 16 Nat
161160biimpa 471 . . . . . . . . . . . . . . 15 Nat
162146, 161nat1st2nd 14103 . . . . . . . . . . . . . 14 Nat
163146, 162, 7natfn 14106 . . . . . . . . . . . . 13
164147adantr 452 . . . . . . . . . . . . . . . . . . 19
165152adantr 452 . . . . . . . . . . . . . . . . . . 19
166 simpr 448 . . . . . . . . . . . . . . . . . . 19
16710, 6, 164, 165, 111, 166yon11 14316 . . . . . . . . . . . . . . . . . 18
168167eleq2d 2471 . . . . . . . . . . . . . . . . 17
169168biimpa 471 . . . . . . . . . . . . . . . 16
170164adantr 452 . . . . . . . . . . . . . . . . . 18
171148ad2antrr 707 . . . . . . . . . . . . . . . . . 18
172149ad2antrr 707 . . . . . . . . . . . . . . . . . 18 f
173150ad2antrr 707 . . . . . . . . . . . . . . . . . 18 f
174151ad2antrr 707 . . . . . . . . . . . . . . . . . 18
175165adantr 452 . . . . . . . . . . . . . . . . . 18
176156ad2antrr 707 . . . . . . . . . . . . . . . . . 18
177 simplr 732 . . . . . . . . . . . . . . . . . 18
178 simpr 448 . . . . . . . . . . . . . . . . . 18
17910, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 170, 171, 172, 173, 174, 175, 42, 176, 177, 178yonedalem4b 14328 . . . . . . . . . . . . . . . . 17
18010, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 170, 171, 172, 173, 174, 175, 26yonedalem3a 14326 . . . . . . . . . . . . . . . . . . . . 21 Nat
181180simpld 446 . . . . . . . . . . . . . . . . . . . 20 Nat
182181fveq1d 5689 . . . . . . . . . . . . . . . . . . 19 Nat
183161ad2antrr 707 . . . . . . . . . . . . . . . . . . . 20 Nat
184 fveq1 5686 . . . . . . . . . . . . . . . . . . . . . 22
185184fveq1d 5689 . . . . . . . . . . . . . . . . . . . . 21
186 fvex 5701 . . . . . . . . . . . . . . . . . . . . 21
187185, 106, 186fvmpt 5765 . . . . . . . . . . . . . . . . . . . 20 Nat Nat
188183, 187syl 16 . . . . . . . . . . . . . . . . . . 19 Nat
189182, 188eqtrd 2436 . . . . . . . . . . . . . . . . . 18
190189fveq2d 5691 . . . . . . . . . . . . . . . . 17
191162ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . 22 Nat
192 eqid 2404 . . . . . . . . . . . . . . . . . . . . . 22
193 eqid 2404 . . . . . . . . . . . . . . . . . . . . . 22 comp comp
194111, 5oppchom 13896 . . . . . . . . . . . . . . . . . . . . . . 23
195178, 194syl6eleqr 2495 . . . . . . . . . . . . . . . . . . . . . 22
196146, 191, 7, 192, 193, 175, 177, 195nati 14107 . . . . . . . . . . . . . . . . . . . . 21 comp comp
19779ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . 24
198197adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23
199198adantr 452 . . . . . . . . . . . . . . . . . . . . . 22
200 relfunc 14014 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
20110, 17, 5, 12, 3, 79, 19yoncl 14314 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
202 1st2ndbr 6355 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
203200, 201, 202sylancr 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
2046, 4, 203funcf1 14018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
205204ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
206205, 152ffvelrnd 5830 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
207 1st2ndbr 6355 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
208116, 206, 207sylancr 645 . . . . . . . . . . . . . . . . . . . . . . . . . 26
2097, 125, 208funcf1 14018 . . . . . . . . . . . . . . . . . . . . . . . . 25
210 eqidd 2405 . . . . . . . . . . . . . . . . . . . . . . . . . 26
21112, 197setcbas 14188 . . . . . . . . . . . . . . . . . . . . . . . . . 26
212210, 211feq23d 5547 . . . . . . . . . . . . . . . . . . . . . . . . 25
213209, 212mpbird 224 . . . . . . . . . . . . . . . . . . . . . . . 24
214213, 152ffvelrnd 5830 . . . . . . . . . . . . . . . . . . . . . . 23
215214ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . 22
216213ffvelrnda 5829 . . . . . . . . . . . . . . . . . . . . . . 23
217216adantr 452 . . . . . . . . . . . . . . . . . . . . . 22
218116, 151, 117sylancr 645 . . . . . . . . . . . . . . . . . . . . . . . . . 26
2197, 125, 218funcf1 14018 . . . . . . . . . . . . . . . . . . . . . . . . 25
220210, 211feq23d 5547 . . . . . . . . . . . . . . . . . . . . . . . . 25
221219, 220mpbird 224 . . . . . . . . . . . . . . . . . . . . . . . 24
222221ffvelrnda 5829 . . . . . . . . . . . . . . . . . . . . . . 23
223222adantr 452 . . . . . . . . . . . . . . . . . . . . . 22
224 eqid 2404 . . . . . . . . . . . . . . . . . . . . . . . . 25
225208ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . 25
2267, 192, 224, 225, 175, 177funcf2 14020 . . . . . . . . . . . . . . . . . . . . . . . 24
227226, 195ffvelrnd 5830 . . . . . . . . . . . . . . . . . . . . . . 23
22812, 199, 224, 215, 217elsetchom 14191 . . . . . . . . . . . . . . . . . . . . . . 23
229227, 228mpbid 202 . . . . . . . . . . . . . . . . . . . . . 22
230162adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . 25 Nat
231146, 230, 7, 224, 166natcl 14105 . . . . . . . . . . . . . . . . . . . . . . . 24
23212, 198, 224, 216, 222elsetchom 14191 . . . . . . . . . . . . . . . . . . . . . . . 24
233231, 232mpbid 202 . . . . . . . . . . . . . . . . . . . . . . 23
234233adantr 452 . . . . . . . . . . . . . . . . . . . . . 22
23512, 199, 193, 215, 217, 223, 229, 234setcco 14193 . . . . . . . . . . . . . . . . . . . . 21 comp
236221, 152ffvelrnd 5830 . . . . . . . . . . . . . . . . . . . . . . 23
237236ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . 22
238146, 162, 7, 224, 152natcl 14105 . . . . . . . . . . . . . . . . . . . . . . . 24
23912, 197, 224, 214, 236elsetchom 14191 . . . . . . . . . . . . . . . . . . . . . . . 24
240238, 239mpbid 202 . . . . . . . . . . . . . . . . . . . . . . 23
241240ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . 22
242116, 174, 117sylancr 645 . . . . . . . . . . . . . . . . . . . . . . . . 25
2437, 192, 224, 242, 175, 177funcf2 14020 . . . . . . . . . . . . . . . . . . . . . . . 24
244243, 195ffvelrnd 5830 . . . . . . . . . . . . . . . . . . . . . . 23
24512, 199, 224, 237, 223elsetchom 14191 . . . . . . . . . . . . . . . . . . . . . . 23
246244, 245mpbid 202 . . . . . . . . . . . . . . . . . . . . . 22
24712, 199, 193, 215, 237, 223, 241, 246setcco 14193 . . . . . . . . . . . . . . . . . . . . 21 comp
248196, 235, 2473eqtr3d 2444 . . . . . . . . . . . . . . . . . . . 20
249248fveq1d 5689 . . . . . . . . . . . . . . . . . . 19
2506, 111, 11, 147, 152catidcl 13862 . . . . . . . . . . . . . . . . . . . . . 22
25110, 6, 147, 152, 111, 152yon11 14316 . . . . . . . . . . . . . . . . . . . . . 22
252250, 251eleqtrrd 2481 . . . . . . . . . . . . . . . . . . . . 21
253252ad2antrr 707 . . . . . . . . . . . . . . . . . . . 20
254 fvco3 5759 . . . . . . . . . . . . . . . . . . . 20
255229, 253, 254syl2anc 643 . . . . . . . . . . . . . . . . . . 19
256 fvco3 5759 . . . . . . . . . . . . . . . . . . . . 21
257240, 252, 256syl2anc 643 . . . . . . . . . . . . . . . . . . . 20
258257ad2antrr 707 . . . . . . . . . . . . . . . . . . 19
259249, 255, 2583eqtr3d 2444 . . . . . . . . . . . . . . . . . 18
260 eqid 2404 . . . . . . . . . . . . . . . . . . . . 21 comp comp
261250ad2antrr 707 . . . . . . . . . . . . . . . . . . . . 21
26210, 6, 170, 175, 111, 175, 260, 177, 178, 261yon12 14317 . . . . . . . . . . . . . . . . . . . 20 comp
2636, 111, 11, 170, 177, 260, 175, 178catlid 13863 . . . . . . . . . . . . . . . . . . . 20 comp
264262, 263eqtrd 2436 . . . . . . . . . . . . . . . . . . 19
265264fveq2d 5691 . . . . . . . . . . . . . . . . . 18
266259, 265eqtr3d 2438 . . . . . . . . . . . . . . . . 17
267179, 190, 2663eqtrd 2440 . . . . . . . . . . . . . . . 16
268169, 267syldan 457 . . . . . . . . . . . . . . 15
269268mpteq2dva 4255 . . . . . . . . . . . . . 14
270158adantr 452 . . . . . . . . . . . . . . . . 17 Nat
271146, 270, 7, 224, 166natcl 14105 . . . . . . . . . . . . . . . 16
27212, 198, 224, 216, 222elsetchom 14191 . . . . . . . . . . . . . . . 16
273271, 272mpbid 202 . . . . . . . . . . . . . . 15
274273feqmptd 5738 . . . . . . . . . . . . . 14
275233feqmptd 5738 . . . . . . . . . . . . . 14
276269, 274, 2753eqtr4d 2446 . . . . . . . . . . . . 13
277159, 163, 276eqfnfvd 5789 . . . . . . . . . . . 12
278277mpteq2dva 4255 . . . . . . . . . . 11
279 mptresid 5154 . . . . . . . . . . 11
280278, 279syl6eq 2452 . . . . . . . . . 10
281145, 280eqtrd 2436 . . . . . . . . 9
282 fcof1o 5985 . . . . . . . . 9