Step | Hyp | Ref
| Expression |
1 | | yoneda.m |
. . . . 5
Nat |
2 | | ovex 6678 |
. . . . . 6
Nat |
3 | 2 | mptex 6486 |
. . . . 5
Nat |
4 | 1, 3 | fnmpt2i 7239 |
. . . 4
|
5 | 4 | a1i 11 |
. . 3
|
6 | | yoneda.y |
. . . . . . . 8
Yon |
7 | | yoneda.b |
. . . . . . . 8
|
8 | | yoneda.1 |
. . . . . . . 8
|
9 | | yoneda.o |
. . . . . . . 8
oppCat |
10 | | yoneda.s |
. . . . . . . 8
|
11 | | yoneda.t |
. . . . . . . 8
|
12 | | yoneda.q |
. . . . . . . 8
FuncCat
|
13 | | yoneda.h |
. . . . . . . 8
HomF |
14 | | yoneda.r |
. . . . . . . 8
c FuncCat |
15 | | yoneda.e |
. . . . . . . 8
evalF |
16 | | yoneda.z |
. . . . . . . 8
func
tpos
func
F
〈,〉F F
|
17 | | yoneda.c |
. . . . . . . . 9
|
18 | 17 | adantr 481 |
. . . . . . . 8
|
19 | | yoneda.w |
. . . . . . . . 9
|
20 | 19 | adantr 481 |
. . . . . . . 8
|
21 | | yoneda.u |
. . . . . . . . 9
f
|
22 | 21 | adantr 481 |
. . . . . . . 8
f |
23 | | yoneda.v |
. . . . . . . . 9
f
|
24 | 23 | adantr 481 |
. . . . . . . 8
f |
25 | | simprl 794 |
. . . . . . . 8
|
26 | | simprr 796 |
. . . . . . . 8
|
27 | 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 18, 20, 22, 24, 25, 26, 1 | yonedalem3a 16914 |
. . . . . . 7
Nat |
28 | 27 | simprd 479 |
. . . . . 6
|
29 | | eqid 2622 |
. . . . . . 7
|
30 | | eqid 2622 |
. . . . . . . . . . 11
c c |
31 | 12 | fucbas 16620 |
. . . . . . . . . . 11
|
32 | 9, 7 | oppcbas 16378 |
. . . . . . . . . . 11
|
33 | 30, 31, 32 | xpcbas 16818 |
. . . . . . . . . 10
c |
34 | | eqid 2622 |
. . . . . . . . . 10
|
35 | | relfunc 16522 |
. . . . . . . . . . 11
c |
36 | 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 19, 21, 23 | yonedalem1 16912 |
. . . . . . . . . . . 12
c c
|
37 | 36 | simpld 475 |
. . . . . . . . . . 11
c |
38 | | 1st2ndbr 7217 |
. . . . . . . . . . 11
c
c
c |
39 | 35, 37, 38 | sylancr 695 |
. . . . . . . . . 10
c |
40 | 33, 34, 39 | funcf1 16526 |
. . . . . . . . 9
|
41 | 40 | fovrnda 6805 |
. . . . . . . 8
|
42 | 11, 20 | setcbas 16728 |
. . . . . . . 8
|
43 | 41, 42 | eleqtrrd 2704 |
. . . . . . 7
|
44 | 36 | simprd 479 |
. . . . . . . . . . 11
c |
45 | | 1st2ndbr 7217 |
. . . . . . . . . . 11
c
c
c |
46 | 35, 44, 45 | sylancr 695 |
. . . . . . . . . 10
c |
47 | 33, 34, 46 | funcf1 16526 |
. . . . . . . . 9
|
48 | 47 | fovrnda 6805 |
. . . . . . . 8
|
49 | 48, 42 | eleqtrrd 2704 |
. . . . . . 7
|
50 | 11, 20, 29, 43, 49 | elsetchom 16731 |
. . . . . 6
|
51 | 28, 50 | mpbird 247 |
. . . . 5
|
52 | 51 | ralrimivva 2971 |
. . . 4
|
53 | | fveq2 6191 |
. . . . . . 7
|
54 | | df-ov 6653 |
. . . . . . 7
|
55 | 53, 54 | syl6eqr 2674 |
. . . . . 6
|
56 | | fveq2 6191 |
. . . . . . . 8
|
57 | | df-ov 6653 |
. . . . . . . 8
|
58 | 56, 57 | syl6eqr 2674 |
. . . . . . 7
|
59 | | fveq2 6191 |
. . . . . . . 8
|
60 | | df-ov 6653 |
. . . . . . . 8
|
61 | 59, 60 | syl6eqr 2674 |
. . . . . . 7
|
62 | 58, 61 | oveq12d 6668 |
. . . . . 6
|
63 | 55, 62 | eleq12d 2695 |
. . . . 5
|
64 | 63 | ralxp 5263 |
. . . 4
|
65 | 52, 64 | sylibr 224 |
. . 3
|
66 | | ovex 6678 |
. . . . . 6
|
67 | | fvex 6201 |
. . . . . . 7
|
68 | 7, 67 | eqeltri 2697 |
. . . . . 6
|
69 | 66, 68 | mpt2ex 7247 |
. . . . 5
Nat |
70 | 1, 69 | eqeltri 2697 |
. . . 4
|
71 | 70 | elixp 7915 |
. . 3
|
72 | 5, 65, 71 | sylanbrc 698 |
. 2
|
73 | 17 | adantr 481 |
. . . . 5
c
|
74 | 19 | adantr 481 |
. . . . 5
c
|
75 | 21 | adantr 481 |
. . . . 5
c
f |
76 | 23 | adantr 481 |
. . . . 5
c
f |
77 | | simpr1 1067 |
. . . . . 6
c
|
78 | | xp1st 7198 |
. . . . . 6
|
79 | 77, 78 | syl 17 |
. . . . 5
c |
80 | | xp2nd 7199 |
. . . . . 6
|
81 | 77, 80 | syl 17 |
. . . . 5
c |
82 | | simpr2 1068 |
. . . . . 6
c
|
83 | | xp1st 7198 |
. . . . . 6
|
84 | 82, 83 | syl 17 |
. . . . 5
c |
85 | | xp2nd 7199 |
. . . . . 6
|
86 | 82, 85 | syl 17 |
. . . . 5
c |
87 | | simpr3 1069 |
. . . . . . 7
c c |
88 | | eqid 2622 |
. . . . . . . . . 10
Nat Nat |
89 | 12, 88 | fuchom 16621 |
. . . . . . . . 9
Nat |
90 | | eqid 2622 |
. . . . . . . . 9
|
91 | | eqid 2622 |
. . . . . . . . 9
c c |
92 | 30, 33, 89, 90, 91, 77, 82 | xpchom 16820 |
. . . . . . . 8
c c Nat |
93 | | eqid 2622 |
. . . . . . . . . 10
|
94 | 93, 9 | oppchom 16375 |
. . . . . . . . 9
|
95 | 94 | xpeq2i 5136 |
. . . . . . . 8
Nat Nat |
96 | 92, 95 | syl6eq 2672 |
. . . . . . 7
c c Nat |
97 | 87, 96 | eleqtrd 2703 |
. . . . . 6
c Nat |
98 | | xp1st 7198 |
. . . . . 6
Nat Nat |
99 | 97, 98 | syl 17 |
. . . . 5
c Nat |
100 | | xp2nd 7199 |
. . . . . 6
Nat |
101 | 97, 100 | syl 17 |
. . . . 5
c |
102 | 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 73, 74, 75, 76, 79, 81, 84, 86, 99, 101, 1 | yonedalem3b 16919 |
. . . 4
c comp comp |
103 | | 1st2nd2 7205 |
. . . . . . . . . 10
|
104 | 77, 103 | syl 17 |
. . . . . . . . 9
c |
105 | 104 | fveq2d 6195 |
. . . . . . . 8
c |
106 | | df-ov 6653 |
. . . . . . . 8
|
107 | 105, 106 | syl6eqr 2674 |
. . . . . . 7
c |
108 | | 1st2nd2 7205 |
. . . . . . . . . 10
|
109 | 82, 108 | syl 17 |
. . . . . . . . 9
c
|
110 | 109 | fveq2d 6195 |
. . . . . . . 8
c |
111 | | df-ov 6653 |
. . . . . . . 8
|
112 | 110, 111 | syl6eqr 2674 |
. . . . . . 7
c |
113 | 107, 112 | opeq12d 4410 |
. . . . . 6
c |
114 | 109 | fveq2d 6195 |
. . . . . . 7
c |
115 | | df-ov 6653 |
. . . . . . 7
|
116 | 114, 115 | syl6eqr 2674 |
. . . . . 6
c |
117 | 113, 116 | oveq12d 6668 |
. . . . 5
c comp comp |
118 | 109 | fveq2d 6195 |
. . . . . 6
c |
119 | | df-ov 6653 |
. . . . . 6
|
120 | 118, 119 | syl6eqr 2674 |
. . . . 5
c |
121 | 104, 109 | oveq12d 6668 |
. . . . . . 7
c |
122 | | 1st2nd2 7205 |
. . . . . . . 8
Nat |
123 | 97, 122 | syl 17 |
. . . . . . 7
c |
124 | 121, 123 | fveq12d 6197 |
. . . . . 6
c |
125 | | df-ov 6653 |
. . . . . 6
|
126 | 124, 125 | syl6eqr 2674 |
. . . . 5
c |
127 | 117, 120,
126 | oveq123d 6671 |
. . . 4
c comp comp |
128 | 104 | fveq2d 6195 |
. . . . . . . 8
c |
129 | | df-ov 6653 |
. . . . . . . 8
|
130 | 128, 129 | syl6eqr 2674 |
. . . . . . 7
c |
131 | 107, 130 | opeq12d 4410 |
. . . . . 6
c |
132 | 131, 116 | oveq12d 6668 |
. . . . 5
c comp comp |
133 | 104, 109 | oveq12d 6668 |
. . . . . . 7
c |
134 | 133, 123 | fveq12d 6197 |
. . . . . 6
c |
135 | | df-ov 6653 |
. . . . . 6
|
136 | 134, 135 | syl6eqr 2674 |
. . . . 5
c |
137 | 104 | fveq2d 6195 |
. . . . . 6
c |
138 | | df-ov 6653 |
. . . . . 6
|
139 | 137, 138 | syl6eqr 2674 |
. . . . 5
c |
140 | 132, 136,
139 | oveq123d 6671 |
. . . 4
c comp comp |
141 | 102, 127,
140 | 3eqtr4d 2666 |
. . 3
c comp comp |
142 | 141 | ralrimivvva 2972 |
. 2
c comp comp |
143 | | eqid 2622 |
. . 3
c Nat c Nat |
144 | | eqid 2622 |
. . 3
comp comp |
145 | 143, 33, 91, 29, 144, 37, 44 | isnat2 16608 |
. 2
c Nat
c comp comp |
146 | 72, 142, 145 | mpbir2and 957 |
1
c Nat |