Metamath Proof Explorer


Theorem yonedalem3

Description: Lemma for yoneda . (Contributed by Mario Carneiro, 28-Jan-2017)

Ref Expression
Hypotheses yoneda.y Y = Yon C
yoneda.b B = Base C
yoneda.1 1 ˙ = Id C
yoneda.o O = oppCat C
yoneda.s S = SetCat U
yoneda.t T = SetCat V
yoneda.q Q = O FuncCat S
yoneda.h H = Hom F Q
yoneda.r R = Q × c O FuncCat T
yoneda.e E = O eval F S
yoneda.z Z = H func 1 st Y tpos 2 nd Y func Q 2 nd F O ⟨,⟩ F Q 1 st F O
yoneda.c φ C Cat
yoneda.w φ V W
yoneda.u φ ran Hom 𝑓 C U
yoneda.v φ ran Hom 𝑓 Q U V
yoneda.m M = f O Func S , x B a 1 st Y x O Nat S f a x 1 ˙ x
Assertion yonedalem3 φ M Z Q × c O Nat T E

Proof

Step Hyp Ref Expression
1 yoneda.y Y = Yon C
2 yoneda.b B = Base C
3 yoneda.1 1 ˙ = Id C
4 yoneda.o O = oppCat C
5 yoneda.s S = SetCat U
6 yoneda.t T = SetCat V
7 yoneda.q Q = O FuncCat S
8 yoneda.h H = Hom F Q
9 yoneda.r R = Q × c O FuncCat T
10 yoneda.e E = O eval F S
11 yoneda.z Z = H func 1 st Y tpos 2 nd Y func Q 2 nd F O ⟨,⟩ F Q 1 st F O
12 yoneda.c φ C Cat
13 yoneda.w φ V W
14 yoneda.u φ ran Hom 𝑓 C U
15 yoneda.v φ ran Hom 𝑓 Q U V
16 yoneda.m M = f O Func S , x B a 1 st Y x O Nat S f a x 1 ˙ x
17 ovex 1 st Y x O Nat S f V
18 17 mptex a 1 st Y x O Nat S f a x 1 ˙ x V
19 16 18 fnmpoi M Fn O Func S × B
20 19 a1i φ M Fn O Func S × B
21 12 adantr φ g O Func S y B C Cat
22 13 adantr φ g O Func S y B V W
23 14 adantr φ g O Func S y B ran Hom 𝑓 C U
24 15 adantr φ g O Func S y B ran Hom 𝑓 Q U V
25 simprl φ g O Func S y B g O Func S
26 simprr φ g O Func S y B y B
27 1 2 3 4 5 6 7 8 9 10 11 21 22 23 24 25 26 16 yonedalem3a φ g O Func S y B g M y = a 1 st Y y O Nat S g a y 1 ˙ y g M y : g 1 st Z y g 1 st E y
28 27 simprd φ g O Func S y B g M y : g 1 st Z y g 1 st E y
29 eqid Hom T = Hom T
30 eqid Q × c O = Q × c O
31 7 fucbas O Func S = Base Q
32 4 2 oppcbas B = Base O
33 30 31 32 xpcbas O Func S × B = Base Q × c O
34 eqid Base T = Base T
35 relfunc Rel Q × c O Func T
36 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 yonedalem1 φ Z Q × c O Func T E Q × c O Func T
37 36 simpld φ Z Q × c O Func T
38 1st2ndbr Rel Q × c O Func T Z Q × c O Func T 1 st Z Q × c O Func T 2 nd Z
39 35 37 38 sylancr φ 1 st Z Q × c O Func T 2 nd Z
40 33 34 39 funcf1 φ 1 st Z : O Func S × B Base T
41 40 fovrnda φ g O Func S y B g 1 st Z y Base T
42 6 22 setcbas φ g O Func S y B V = Base T
43 41 42 eleqtrrd φ g O Func S y B g 1 st Z y V
44 36 simprd φ E Q × c O Func T
45 1st2ndbr Rel Q × c O Func T E Q × c O Func T 1 st E Q × c O Func T 2 nd E
46 35 44 45 sylancr φ 1 st E Q × c O Func T 2 nd E
47 33 34 46 funcf1 φ 1 st E : O Func S × B Base T
48 47 fovrnda φ g O Func S y B g 1 st E y Base T
49 48 42 eleqtrrd φ g O Func S y B g 1 st E y V
50 6 22 29 43 49 elsetchom φ g O Func S y B g M y g 1 st Z y Hom T g 1 st E y g M y : g 1 st Z y g 1 st E y
51 28 50 mpbird φ g O Func S y B g M y g 1 st Z y Hom T g 1 st E y
52 51 ralrimivva φ g O Func S y B g M y g 1 st Z y Hom T g 1 st E y
53 fveq2 z = g y M z = M g y
54 df-ov g M y = M g y
55 53 54 eqtr4di z = g y M z = g M y
56 fveq2 z = g y 1 st Z z = 1 st Z g y
57 df-ov g 1 st Z y = 1 st Z g y
58 56 57 eqtr4di z = g y 1 st Z z = g 1 st Z y
59 fveq2 z = g y 1 st E z = 1 st E g y
60 df-ov g 1 st E y = 1 st E g y
61 59 60 eqtr4di z = g y 1 st E z = g 1 st E y
62 58 61 oveq12d z = g y 1 st Z z Hom T 1 st E z = g 1 st Z y Hom T g 1 st E y
63 55 62 eleq12d z = g y M z 1 st Z z Hom T 1 st E z g M y g 1 st Z y Hom T g 1 st E y
64 63 ralxp z O Func S × B M z 1 st Z z Hom T 1 st E z g O Func S y B g M y g 1 st Z y Hom T g 1 st E y
65 52 64 sylibr φ z O Func S × B M z 1 st Z z Hom T 1 st E z
66 ovex O Func S V
67 2 fvexi B V
68 66 67 mpoex f O Func S , x B a 1 st Y x O Nat S f a x 1 ˙ x V
69 16 68 eqeltri M V
70 69 elixp M z O Func S × B 1 st Z z Hom T 1 st E z M Fn O Func S × B z O Func S × B M z 1 st Z z Hom T 1 st E z
71 20 65 70 sylanbrc φ M z O Func S × B 1 st Z z Hom T 1 st E z
72 12 adantr φ z O Func S × B w O Func S × B g z Hom Q × c O w C Cat
73 13 adantr φ z O Func S × B w O Func S × B g z Hom Q × c O w V W
74 14 adantr φ z O Func S × B w O Func S × B g z Hom Q × c O w ran Hom 𝑓 C U
75 15 adantr φ z O Func S × B w O Func S × B g z Hom Q × c O w ran Hom 𝑓 Q U V
76 simpr1 φ z O Func S × B w O Func S × B g z Hom Q × c O w z O Func S × B
77 xp1st z O Func S × B 1 st z O Func S
78 76 77 syl φ z O Func S × B w O Func S × B g z Hom Q × c O w 1 st z O Func S
79 xp2nd z O Func S × B 2 nd z B
80 76 79 syl φ z O Func S × B w O Func S × B g z Hom Q × c O w 2 nd z B
81 simpr2 φ z O Func S × B w O Func S × B g z Hom Q × c O w w O Func S × B
82 xp1st w O Func S × B 1 st w O Func S
83 81 82 syl φ z O Func S × B w O Func S × B g z Hom Q × c O w 1 st w O Func S
84 xp2nd w O Func S × B 2 nd w B
85 81 84 syl φ z O Func S × B w O Func S × B g z Hom Q × c O w 2 nd w B
86 simpr3 φ z O Func S × B w O Func S × B g z Hom Q × c O w g z Hom Q × c O w
87 eqid O Nat S = O Nat S
88 7 87 fuchom O Nat S = Hom Q
89 eqid Hom O = Hom O
90 eqid Hom Q × c O = Hom Q × c O
91 30 33 88 89 90 76 81 xpchom φ z O Func S × B w O Func S × B g z Hom Q × c O w z Hom Q × c O w = 1 st z O Nat S 1 st w × 2 nd z Hom O 2 nd w
92 eqid Hom C = Hom C
93 92 4 oppchom 2 nd z Hom O 2 nd w = 2 nd w Hom C 2 nd z
94 93 xpeq2i 1 st z O Nat S 1 st w × 2 nd z Hom O 2 nd w = 1 st z O Nat S 1 st w × 2 nd w Hom C 2 nd z
95 91 94 eqtrdi φ z O Func S × B w O Func S × B g z Hom Q × c O w z Hom Q × c O w = 1 st z O Nat S 1 st w × 2 nd w Hom C 2 nd z
96 86 95 eleqtrd φ z O Func S × B w O Func S × B g z Hom Q × c O w g 1 st z O Nat S 1 st w × 2 nd w Hom C 2 nd z
97 xp1st g 1 st z O Nat S 1 st w × 2 nd w Hom C 2 nd z 1 st g 1 st z O Nat S 1 st w
98 96 97 syl φ z O Func S × B w O Func S × B g z Hom Q × c O w 1 st g 1 st z O Nat S 1 st w
99 xp2nd g 1 st z O Nat S 1 st w × 2 nd w Hom C 2 nd z 2 nd g 2 nd w Hom C 2 nd z
100 96 99 syl φ z O Func S × B w O Func S × B g z Hom Q × c O w 2 nd g 2 nd w Hom C 2 nd z
101 1 2 3 4 5 6 7 8 9 10 11 72 73 74 75 78 80 83 85 98 100 16 yonedalem3b φ z O Func S × B w O Func S × B g z Hom Q × c O w 1 st w M 2 nd w 1 st z 1 st Z 2 nd z 1 st w 1 st Z 2 nd w comp T 1 st w 1 st E 2 nd w 1 st g 1 st z 2 nd z 2 nd Z 1 st w 2 nd w 2 nd g = 1 st g 1 st z 2 nd z 2 nd E 1 st w 2 nd w 2 nd g 1 st z 1 st Z 2 nd z 1 st z 1 st E 2 nd z comp T 1 st w 1 st E 2 nd w 1 st z M 2 nd z
102 1st2nd2 z O Func S × B z = 1 st z 2 nd z
103 76 102 syl φ z O Func S × B w O Func S × B g z Hom Q × c O w z = 1 st z 2 nd z
104 103 fveq2d φ z O Func S × B w O Func S × B g z Hom Q × c O w 1 st Z z = 1 st Z 1 st z 2 nd z
105 df-ov 1 st z 1 st Z 2 nd z = 1 st Z 1 st z 2 nd z
106 104 105 eqtr4di φ z O Func S × B w O Func S × B g z Hom Q × c O w 1 st Z z = 1 st z 1 st Z 2 nd z
107 1st2nd2 w O Func S × B w = 1 st w 2 nd w
108 81 107 syl φ z O Func S × B w O Func S × B g z Hom Q × c O w w = 1 st w 2 nd w
109 108 fveq2d φ z O Func S × B w O Func S × B g z Hom Q × c O w 1 st Z w = 1 st Z 1 st w 2 nd w
110 df-ov 1 st w 1 st Z 2 nd w = 1 st Z 1 st w 2 nd w
111 109 110 eqtr4di φ z O Func S × B w O Func S × B g z Hom Q × c O w 1 st Z w = 1 st w 1 st Z 2 nd w
112 106 111 opeq12d φ z O Func S × B w O Func S × B g z Hom Q × c O w 1 st Z z 1 st Z w = 1 st z 1 st Z 2 nd z 1 st w 1 st Z 2 nd w
113 108 fveq2d φ z O Func S × B w O Func S × B g z Hom Q × c O w 1 st E w = 1 st E 1 st w 2 nd w
114 df-ov 1 st w 1 st E 2 nd w = 1 st E 1 st w 2 nd w
115 113 114 eqtr4di φ z O Func S × B w O Func S × B g z Hom Q × c O w 1 st E w = 1 st w 1 st E 2 nd w
116 112 115 oveq12d φ z O Func S × B w O Func S × B g z Hom Q × c O w 1 st Z z 1 st Z w comp T 1 st E w = 1 st z 1 st Z 2 nd z 1 st w 1 st Z 2 nd w comp T 1 st w 1 st E 2 nd w
117 108 fveq2d φ z O Func S × B w O Func S × B g z Hom Q × c O w M w = M 1 st w 2 nd w
118 df-ov 1 st w M 2 nd w = M 1 st w 2 nd w
119 117 118 eqtr4di φ z O Func S × B w O Func S × B g z Hom Q × c O w M w = 1 st w M 2 nd w
120 103 108 oveq12d φ z O Func S × B w O Func S × B g z Hom Q × c O w z 2 nd Z w = 1 st z 2 nd z 2 nd Z 1 st w 2 nd w
121 1st2nd2 g 1 st z O Nat S 1 st w × 2 nd w Hom C 2 nd z g = 1 st g 2 nd g
122 96 121 syl φ z O Func S × B w O Func S × B g z Hom Q × c O w g = 1 st g 2 nd g
123 120 122 fveq12d φ z O Func S × B w O Func S × B g z Hom Q × c O w z 2 nd Z w g = 1 st z 2 nd z 2 nd Z 1 st w 2 nd w 1 st g 2 nd g
124 df-ov 1 st g 1 st z 2 nd z 2 nd Z 1 st w 2 nd w 2 nd g = 1 st z 2 nd z 2 nd Z 1 st w 2 nd w 1 st g 2 nd g
125 123 124 eqtr4di φ z O Func S × B w O Func S × B g z Hom Q × c O w z 2 nd Z w g = 1 st g 1 st z 2 nd z 2 nd Z 1 st w 2 nd w 2 nd g
126 116 119 125 oveq123d φ z O Func S × B w O Func S × B g z Hom Q × c O w M w 1 st Z z 1 st Z w comp T 1 st E w z 2 nd Z w g = 1 st w M 2 nd w 1 st z 1 st Z 2 nd z 1 st w 1 st Z 2 nd w comp T 1 st w 1 st E 2 nd w 1 st g 1 st z 2 nd z 2 nd Z 1 st w 2 nd w 2 nd g
127 103 fveq2d φ z O Func S × B w O Func S × B g z Hom Q × c O w 1 st E z = 1 st E 1 st z 2 nd z
128 df-ov 1 st z 1 st E 2 nd z = 1 st E 1 st z 2 nd z
129 127 128 eqtr4di φ z O Func S × B w O Func S × B g z Hom Q × c O w 1 st E z = 1 st z 1 st E 2 nd z
130 106 129 opeq12d φ z O Func S × B w O Func S × B g z Hom Q × c O w 1 st Z z 1 st E z = 1 st z 1 st Z 2 nd z 1 st z 1 st E 2 nd z
131 130 115 oveq12d φ z O Func S × B w O Func S × B g z Hom Q × c O w 1 st Z z 1 st E z comp T 1 st E w = 1 st z 1 st Z 2 nd z 1 st z 1 st E 2 nd z comp T 1 st w 1 st E 2 nd w
132 103 108 oveq12d φ z O Func S × B w O Func S × B g z Hom Q × c O w z 2 nd E w = 1 st z 2 nd z 2 nd E 1 st w 2 nd w
133 132 122 fveq12d φ z O Func S × B w O Func S × B g z Hom Q × c O w z 2 nd E w g = 1 st z 2 nd z 2 nd E 1 st w 2 nd w 1 st g 2 nd g
134 df-ov 1 st g 1 st z 2 nd z 2 nd E 1 st w 2 nd w 2 nd g = 1 st z 2 nd z 2 nd E 1 st w 2 nd w 1 st g 2 nd g
135 133 134 eqtr4di φ z O Func S × B w O Func S × B g z Hom Q × c O w z 2 nd E w g = 1 st g 1 st z 2 nd z 2 nd E 1 st w 2 nd w 2 nd g
136 103 fveq2d φ z O Func S × B w O Func S × B g z Hom Q × c O w M z = M 1 st z 2 nd z
137 df-ov 1 st z M 2 nd z = M 1 st z 2 nd z
138 136 137 eqtr4di φ z O Func S × B w O Func S × B g z Hom Q × c O w M z = 1 st z M 2 nd z
139 131 135 138 oveq123d φ z O Func S × B w O Func S × B g z Hom Q × c O w z 2 nd E w g 1 st Z z 1 st E z comp T 1 st E w M z = 1 st g 1 st z 2 nd z 2 nd E 1 st w 2 nd w 2 nd g 1 st z 1 st Z 2 nd z 1 st z 1 st E 2 nd z comp T 1 st w 1 st E 2 nd w 1 st z M 2 nd z
140 101 126 139 3eqtr4d φ z O Func S × B w O Func S × B g z Hom Q × c O w M w 1 st Z z 1 st Z w comp T 1 st E w z 2 nd Z w g = z 2 nd E w g 1 st Z z 1 st E z comp T 1 st E w M z
141 140 ralrimivvva φ z O Func S × B w O Func S × B g z Hom Q × c O w M w 1 st Z z 1 st Z w comp T 1 st E w z 2 nd Z w g = z 2 nd E w g 1 st Z z 1 st E z comp T 1 st E w M z
142 eqid Q × c O Nat T = Q × c O Nat T
143 eqid comp T = comp T
144 142 33 90 29 143 37 44 isnat2 φ M Z Q × c O Nat T E M z O Func S × B 1 st Z z Hom T 1 st E z z O Func S × B w O Func S × B g z Hom Q × c O w M w 1 st Z z 1 st Z w comp T 1 st E w z 2 nd Z w g = z 2 nd E w g 1 st Z z 1 st E z comp T 1 st E w M z
145 71 141 144 mpbir2and φ M Z Q × c O Nat T E