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

Theorem yonedainv 14429
Description: The Yoneda Lemma with explicit inverse. (Contributed by Mario Carneiro, 29-Jan-2017.)
Hypotheses
Ref Expression
yoneda.y
yoneda.b
yoneda.1
yoneda.o
yoneda.s
yoneda.t
yoneda.q
yoneda.h
yoneda.r
yoneda.e
yoneda.z
yoneda.c
yoneda.w
yoneda.u
yoneda.v
yoneda.m
yonedainv.i
yonedainv.n
Assertion
Ref Expression
yonedainv
Distinct variable groups:   , , , , ,   , , , , , ,   , , , , ,   , , , , , ,   N,   O, , , , , ,   S, , , , , ,   ,M, ,   Q, , , , ,   , , , ,   , , , , , ,   ,   , , , , , ,   , , , , , ,
Allowed substitution hints:   Q( )   ( , , , , )   ( , )   ( , , , , , )   ( )   ( )   ( , , , , , )   I( , , , , , )   M( , , )   N( , , , , )   ( , , , , , )   ( , , , , , )

Proof of Theorem yonedainv
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 yoneda.r . . 3
2 eqid 2443 . . . 4
3 yoneda.q . . . . 5
43fucbas 14208 . . . 4
5 yoneda.o . . . . 5
6 yoneda.b . . . . 5
75, 6oppcbas 13995 . . . 4
82, 4, 7xpcbas 14326 . . 3
9 eqid 2443 . . 3
10 yoneda.y . . . . 5
11 yoneda.1 . . . . 5
12 yoneda.s . . . . 5
13 yoneda.t . . . . 5
14 yoneda.h . . . . 5
15 yoneda.e . . . . 5
16 yoneda.z . . . . 5
17 yoneda.c . . . . 5
18 yoneda.w . . . . 5
19 yoneda.u . . . . 5
20 yoneda.v . . . . 5
2110, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 17, 18, 19, 20yonedalem1 14420 . . . 4
2221simpld 447 . . 3
2321simprd 451 . . 3
24 yonedainv.i . . 3
25 eqid 2443 . . 3
26 yoneda.m . . . 4
2710, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 17, 18, 19, 20, 26yonedalem3 14428 . . 3
2817adantr 453 . . . . . . . . . . 11
2918adantr 453 . . . . . . . . . . 11
3019adantr 453 . . . . . . . . . . 11
3120adantr 453 . . . . . . . . . . 11
32 simprl 734 . . . . . . . . . . 11
33 simprr 735 . . . . . . . . . . 11
3410, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 28, 29, 30, 31, 32, 33, 26yonedalem3a 14422 . . . . . . . . . 10
3534simprd 451 . . . . . . . . 9
3628adantr 453 . . . . . . . . . . . 12
3729adantr 453 . . . . . . . . . . . 12
3830adantr 453 . . . . . . . . . . . 12
3931adantr 453 . . . . . . . . . . . 12
40 simplrl 738 . . . . . . . . . . . 12
41 simplrr 739 . . . . . . . . . . . 12
42 yonedainv.n . . . . . . . . . . . 12
43 simpr 449 . . . . . . . . . . . 12
4410, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 36, 37, 38, 39, 40, 41, 42, 43yonedalem4c 14425 . . . . . . . . . . 11
45 eqid 2443 . . . . . . . . . . 11
4644, 45fmptd 5941 . . . . . . . . . 10
47 fvex 5785 . . . . . . . . . . . . . . . 16
486, 47eqeltri 2513 . . . . . . . . . . . . . . 15
4948mptex 6014 . . . . . . . . . . . . . 14
50 eqid 2443 . . . . . . . . . . . . . 14
5149, 50fnmpti 5620 . . . . . . . . . . . . 13
52 simpl 445 . . . . . . . . . . . . . . . . . . 19
5352fveq2d 5779 . . . . . . . . . . . . . . . . . 18
54 simpr 449 . . . . . . . . . . . . . . . . . 18
5553, 54fveq12d 5781 . . . . . . . . . . . . . . . . 17
56 simplr 733 . . . . . . . . . . . . . . . . . . . 20
5756oveq2d 6145 . . . . . . . . . . . . . . . . . . 19
58 simpll 732 . . . . . . . . . . . . . . . . . . . . . . 23
5958fveq2d 5779 . . . . . . . . . . . . . . . . . . . . . 22
60 eqidd 2444 . . . . . . . . . . . . . . . . . . . . . 22
6159, 56, 60oveq123d 6150 . . . . . . . . . . . . . . . . . . . . 21
6261fveq1d 5777 . . . . . . . . . . . . . . . . . . . 20
6362fveq1d 5777 . . . . . . . . . . . . . . . . . . 19
6457, 63mpteq12dv 4321 . . . . . . . . . . . . . . . . . 18
6564mpteq2dva 4329 . . . . . . . . . . . . . . . . 17
6655, 65mpteq12dv 4321 . . . . . . . . . . . . . . . 16
67 fvex 5785 . . . . . . . . . . . . . . . . 17
6867mptex 6014 . . . . . . . . . . . . . . . 16
6966, 42, 68ovmpt2a 6254 . . . . . . . . . . . . . . 15
7069adantl 454 . . . . . . . . . . . . . 14
7170fneq1d 5583 . . . . . . . . . . . . 13
7251, 71mpbiri 226 . . . . . . . . . . . 12
73 dffn5 5820 . . . . . . . . . . . 12
7472, 73sylib 190 . . . . . . . . . . 11
755oppccat 13999 . . . . . . . . . . . . . 14
7617, 75syl 16 . . . . . . . . . . . . 13
7776adantr 453 . . . . . . . . . . . 12
7820unssbd 3514 . . . . . . . . . . . . . . 15
7918, 78ssexd 4389 . . . . . . . . . . . . . 14
8012setccat 14291 . . . . . . . . . . . . . 14
8179, 80syl 16 . . . . . . . . . . . . 13
8281adantr 453 . . . . . . . . . . . 12
8315, 77, 82, 7, 32, 33evlf1 14368 . . . . . . . . . . 11
8410, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 28, 29, 30, 31, 32, 33yonedalem21 14421 . . . . . . . . . . 11
8574, 83, 84feq123d 5630 . . . . . . . . . 10
8646, 85mpbird 225 . . . . . . . . 9
87 fcompt 5952 . . . . . . . . . . 11
8835, 86, 87syl2anc 644 . . . . . . . . . 10
8983eleq2d 2510 . . . . . . . . . . . . . 14
9089biimpa 472 . . . . . . . . . . . . 13
9128adantr 453 . . . . . . . . . . . . . . . . 17
9229adantr 453 . . . . . . . . . . . . . . . . 17
9330adantr 453 . . . . . . . . . . . . . . . . 17
9431adantr 453 . . . . . . . . . . . . . . . . 17
95 simplrl 738 . . . . . . . . . . . . . . . . 17
96 simplrr 739 . . . . . . . . . . . . . . . . 17
9710, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 91, 92, 93, 94, 95, 96, 26yonedalem3a 14422 . . . . . . . . . . . . . . . 16
9897simpld 447 . . . . . . . . . . . . . . 15
9998fveq1d 5777 . . . . . . . . . . . . . 14
100 fvex 5785 . . . . . . . . . . . . . . . . . 18
101100a1i 11 . . . . . . . . . . . . . . . . 17
102101, 74, 44fmpt2d 5946 . . . . . . . . . . . . . . . 16
103102ffvelrnda 5918 . . . . . . . . . . . . . . 15
104 fveq1 5774 . . . . . . . . . . . . . . . . 17
105104fveq1d 5777 . . . . . . . . . . . . . . . 16
106 eqid 2443 . . . . . . . . . . . . . . . 16
107 fvex 5785 . . . . . . . . . . . . . . . 16
108105, 106, 107fvmpt 5854 . . . . . . . . . . . . . . 15
109103, 108syl 16 . . . . . . . . . . . . . 14
110 simpr 449 . . . . . . . . . . . . . . . 16
111 eqid 2443 . . . . . . . . . . . . . . . . 17
1126, 111, 11, 91, 96catidcl 13958 . . . . . . . . . . . . . . . 16
11310, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 91, 92, 93, 94, 95, 96, 42, 110, 96, 112yonedalem4b 14424 . . . . . . . . . . . . . . 15
114 eqid 2443 . . . . . . . . . . . . . . . . . 18
115 eqid 2443 . . . . . . . . . . . . . . . . . 18
116 relfunc 14110 . . . . . . . . . . . . . . . . . . 19
117 1st2ndbr 6446 . . . . . . . . . . . . . . . . . . 19
118116, 95, 117sylancr 646 . . . . . . . . . . . . . . . . . 18
1197, 114, 115, 118, 96funcid 14118 . . . . . . . . . . . . . . . . 17
1205, 11oppcid 13998 . . . . . . . . . . . . . . . . . . . 20
12191, 120syl 16 . . . . . . . . . . . . . . . . . . 19
122121fveq1d 5777 . . . . . . . . . . . . . . . . . 18
123122fveq2d 5779 . . . . . . . . . . . . . . . . 17
12479ad2antrr 708 . . . . . . . . . . . . . . . . . 18
125 eqid 2443 . . . . . . . . . . . . . . . . . . . . 21
1267, 125, 118funcf1 14114 . . . . . . . . . . . . . . . . . . . 20
127 eqidd 2444 . . . . . . . . . . . . . . . . . . . . 21
12812, 124setcbas 14284 . . . . . . . . . . . . . . . . . . . . 21
129127, 128feq23d 5635 . . . . . . . . . . . . . . . . . . . 20
130126, 129mpbird 225 . . . . . . . . . . . . . . . . . . 19
131130, 96ffvelrnd 5919 . . . . . . . . . . . . . . . . . 18
13212, 115, 124, 131setcid 14292 . . . . . . . . . . . . . . . . 17
133119, 123, 1323eqtr3d 2483 . . . . . . . . . . . . . . . 16
134133fveq1d 5777 . . . . . . . . . . . . . . 15
135 fvresi 5972 . . . . . . . . . . . . . . . 16
136135adantl 454 . . . . . . . . . . . . . . 15
137113, 134, 1363eqtrd 2479 . . . . . . . . . . . . . 14
13899, 109, 1373eqtrd 2479 . . . . . . . . . . . . 13
13990, 138syldan 458 . . . . . . . . . . . 12
140139mpteq2dva 4329 . . . . . . . . . . 11
141 mptresid 5239 . . . . . . . . . . 11
142140, 141syl6eq 2491 . . . . . . . . . 10
14388, 142eqtrd 2475 . . . . . . . . 9
144 fcompt 5952 . . . . . . . . . . 11
14586, 35, 144syl2anc 644 . . . . . . . . . 10
146 eqid 2443 . . . . . . . . . . . . . 14
14728adantr 453 . . . . . . . . . . . . . . . 16
14829adantr 453 . . . . . . . . . . . . . . . 16
14930adantr 453 . . . . . . . . . . . . . . . 16
15031adantr 453 . . . . . . . . . . . . . . . 16
151 simplrl 738 . . . . . . . . . . . . . . . 16
152 simplrr 739 . . . . . . . . . . . . . . . 16
153 eqidd 2444 . . . . . . . . . . . . . . . . . . 19
154153, 83feq23d 5635 . . . . . . . . . . . . . . . . . 18
15535, 154mpbid 203 . . . . . . . . . . . . . . . . 17
156155ffvelrnda 5918 . . . . . . . . . . . . . . . 16
15710, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 147, 148, 149, 150, 151, 152, 42, 156yonedalem4c 14425 . . . . . . . . . . . . . . 15
158146, 157nat1st2nd 14199 . . . . . . . . . . . . . 14
159146, 158, 7natfn 14202 . . . . . . . . . . . . 13
16084eleq2d 2510 . . . . . . . . . . . . . . . 16
161160biimpa 472 . . . . . . . . . . . . . . 15
162146, 161nat1st2nd 14199 . . . . . . . . . . . . . 14
163146, 162, 7natfn 14202 . . . . . . . . . . . . 13
164147adantr 453 . . . . . . . . . . . . . . . . . . 19
165152adantr 453 . . . . . . . . . . . . . . . . . . 19
166 simpr 449 . . . . . . . . . . . . . . . . . . 19
16710, 6, 164, 165, 111, 166yon11 14412 . . . . . . . . . . . . . . . . . 18