Metamath Proof Explorer


Theorem yonffthlem

Description: Lemma for yonffth . (Contributed by Mario Carneiro, 29-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
yonedainv.i I = Inv R
yonedainv.n N = f O Func S , x B u 1 st f x y B g y Hom C x x 2 nd f y g u
Assertion yonffthlem φ Y C Full Q C Faith Q

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 yonedainv.i I = Inv R
18 yonedainv.n N = f O Func S , x B u 1 st f x y B g y Hom C x x 2 nd f y g u
19 relfunc Rel C Func Q
20 15 unssbd φ U V
21 13 20 ssexd φ U V
22 1 12 4 5 7 21 14 yoncl φ Y C Func Q
23 1st2nd Rel C Func Q Y C Func Q Y = 1 st Y 2 nd Y
24 19 22 23 sylancr φ Y = 1 st Y 2 nd Y
25 1st2ndbr Rel C Func Q Y C Func Q 1 st Y C Func Q 2 nd Y
26 19 22 25 sylancr φ 1 st Y C Func Q 2 nd Y
27 fveq2 v = 1 st Y w z N v = N 1 st Y w z
28 df-ov 1 st Y w N z = N 1 st Y w z
29 27 28 eqtr4di v = 1 st Y w z N v = 1 st Y w N z
30 fveq2 v = 1 st Y w z 1 st E v = 1 st E 1 st Y w z
31 df-ov 1 st Y w 1 st E z = 1 st E 1 st Y w z
32 30 31 eqtr4di v = 1 st Y w z 1 st E v = 1 st Y w 1 st E z
33 fveq2 v = 1 st Y w z 1 st Z v = 1 st Z 1 st Y w z
34 df-ov 1 st Y w 1 st Z z = 1 st Z 1 st Y w z
35 33 34 eqtr4di v = 1 st Y w z 1 st Z v = 1 st Y w 1 st Z z
36 32 35 oveq12d v = 1 st Y w z 1 st E v Iso T 1 st Z v = 1 st Y w 1 st E z Iso T 1 st Y w 1 st Z z
37 29 36 eleq12d v = 1 st Y w z N v 1 st E v Iso T 1 st Z v 1 st Y w N z 1 st Y w 1 st E z Iso T 1 st Y w 1 st Z z
38 9 fucbas Q × c O Func T = Base R
39 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
40 39 simpld φ Z Q × c O Func T
41 funcrcl Z Q × c O Func T Q × c O Cat T Cat
42 40 41 syl φ Q × c O Cat T Cat
43 42 simpld φ Q × c O Cat
44 42 simprd φ T Cat
45 9 43 44 fuccat φ R Cat
46 39 simprd φ E Q × c O Func T
47 eqid Iso R = Iso R
48 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 yonedainv φ M Z I E N
49 38 17 45 40 46 47 48 inviso2 φ N E Iso R Z
50 eqid Q × c O = Q × c O
51 7 fucbas O Func S = Base Q
52 4 2 oppcbas B = Base O
53 50 51 52 xpcbas O Func S × B = Base Q × c O
54 eqid Q × c O Nat T = Q × c O Nat T
55 eqid Iso T = Iso T
56 9 53 54 46 40 47 55 fuciso φ N E Iso R Z N E Q × c O Nat T Z v O Func S × B N v 1 st E v Iso T 1 st Z v
57 49 56 mpbid φ N E Q × c O Nat T Z v O Func S × B N v 1 st E v Iso T 1 st Z v
58 57 simprd φ v O Func S × B N v 1 st E v Iso T 1 st Z v
59 58 adantr φ z B w B v O Func S × B N v 1 st E v Iso T 1 st Z v
60 2 51 26 funcf1 φ 1 st Y : B O Func S
61 60 adantr φ z B w B 1 st Y : B O Func S
62 simprr φ z B w B w B
63 61 62 ffvelrnd φ z B w B 1 st Y w O Func S
64 simprl φ z B w B z B
65 63 64 opelxpd φ z B w B 1 st Y w z O Func S × B
66 37 59 65 rspcdva φ z B w B 1 st Y w N z 1 st Y w 1 st E z Iso T 1 st Y w 1 st Z z
67 4 oppccat C Cat O Cat
68 12 67 syl φ O Cat
69 68 adantr φ z B w B O Cat
70 5 setccat U V S Cat
71 21 70 syl φ S Cat
72 71 adantr φ z B w B S Cat
73 10 69 72 52 63 64 evlf1 φ z B w B 1 st Y w 1 st E z = 1 st 1 st Y w z
74 12 adantr φ z B w B C Cat
75 eqid Hom C = Hom C
76 1 2 74 62 75 64 yon11 φ z B w B 1 st 1 st Y w z = z Hom C w
77 73 76 eqtrd φ z B w B 1 st Y w 1 st E z = z Hom C w
78 13 adantr φ z B w B V W
79 14 adantr φ z B w B ran Hom 𝑓 C U
80 15 adantr φ z B w B ran Hom 𝑓 Q U V
81 1 2 3 4 5 6 7 8 9 10 11 74 78 79 80 63 64 yonedalem21 φ z B w B 1 st Y w 1 st Z z = 1 st Y z O Nat S 1 st Y w
82 77 81 oveq12d φ z B w B 1 st Y w 1 st E z Iso T 1 st Y w 1 st Z z = z Hom C w Iso T 1 st Y z O Nat S 1 st Y w
83 66 82 eleqtrd φ z B w B 1 st Y w N z z Hom C w Iso T 1 st Y z O Nat S 1 st Y w
84 20 adantr φ z B w B U V
85 eqid Base S = Base S
86 relfunc Rel O Func S
87 1st2ndbr Rel O Func S 1 st Y w O Func S 1 st 1 st Y w O Func S 2 nd 1 st Y w
88 86 63 87 sylancr φ z B w B 1 st 1 st Y w O Func S 2 nd 1 st Y w
89 52 85 88 funcf1 φ z B w B 1 st 1 st Y w : B Base S
90 89 64 ffvelrnd φ z B w B 1 st 1 st Y w z Base S
91 5 21 setcbas φ U = Base S
92 91 adantr φ z B w B U = Base S
93 90 92 eleqtrrd φ z B w B 1 st 1 st Y w z U
94 76 93 eqeltrrd φ z B w B z Hom C w U
95 84 94 sseldd φ z B w B z Hom C w V
96 eqid Hom 𝑓 Q = Hom 𝑓 Q
97 eqid O Nat S = O Nat S
98 7 97 fuchom O Nat S = Hom Q
99 61 64 ffvelrnd φ z B w B 1 st Y z O Func S
100 96 51 98 99 63 homfval φ z B w B 1 st Y z Hom 𝑓 Q 1 st Y w = 1 st Y z O Nat S 1 st Y w
101 15 unssad φ ran Hom 𝑓 Q V
102 101 adantr φ z B w B ran Hom 𝑓 Q V
103 96 51 homffn Hom 𝑓 Q Fn O Func S × O Func S
104 fnovrn Hom 𝑓 Q Fn O Func S × O Func S 1 st Y z O Func S 1 st Y w O Func S 1 st Y z Hom 𝑓 Q 1 st Y w ran Hom 𝑓 Q
105 103 99 63 104 mp3an2i φ z B w B 1 st Y z Hom 𝑓 Q 1 st Y w ran Hom 𝑓 Q
106 102 105 sseldd φ z B w B 1 st Y z Hom 𝑓 Q 1 st Y w V
107 100 106 eqeltrrd φ z B w B 1 st Y z O Nat S 1 st Y w V
108 6 78 95 107 55 setciso φ z B w B 1 st Y w N z z Hom C w Iso T 1 st Y z O Nat S 1 st Y w 1 st Y w N z : z Hom C w 1-1 onto 1 st Y z O Nat S 1 st Y w
109 83 108 mpbid φ z B w B 1 st Y w N z : z Hom C w 1-1 onto 1 st Y z O Nat S 1 st Y w
110 74 adantr φ z B w B h z Hom C w C Cat
111 110 adantr φ z B w B h z Hom C w y B C Cat
112 64 adantr φ z B w B h z Hom C w z B
113 112 adantr φ z B w B h z Hom C w y B z B
114 simpr φ z B w B h z Hom C w y B y B
115 1 2 111 113 75 114 yon11 φ z B w B h z Hom C w y B 1 st 1 st Y z y = y Hom C z
116 115 eqcomd φ z B w B h z Hom C w y B y Hom C z = 1 st 1 st Y z y
117 111 adantr φ z B w B h z Hom C w y B g y Hom C z C Cat
118 62 ad3antrrr φ z B w B h z Hom C w y B g y Hom C z w B
119 113 adantr φ z B w B h z Hom C w y B g y Hom C z z B
120 eqid comp C = comp C
121 114 adantr φ z B w B h z Hom C w y B g y Hom C z y B
122 simpr φ z B w B h z Hom C w y B g y Hom C z g y Hom C z
123 simpllr φ z B w B h z Hom C w y B g y Hom C z h z Hom C w
124 1 2 117 118 75 119 120 121 122 123 yon12 φ z B w B h z Hom C w y B g y Hom C z z 2 nd 1 st Y w y g h = h y z comp C w g
125 1 2 117 119 75 118 120 121 123 122 yon2 φ z B w B h z Hom C w y B g y Hom C z z 2 nd Y w h y g = h y z comp C w g
126 124 125 eqtr4d φ z B w B h z Hom C w y B g y Hom C z z 2 nd 1 st Y w y g h = z 2 nd Y w h y g
127 116 126 mpteq12dva φ z B w B h z Hom C w y B g y Hom C z z 2 nd 1 st Y w y g h = g 1 st 1 st Y z y z 2 nd Y w h y g
128 26 adantr φ z B w B 1 st Y C Func Q 2 nd Y
129 2 75 98 128 64 62 funcf2 φ z B w B z 2 nd Y w : z Hom C w 1 st Y z O Nat S 1 st Y w
130 129 ffvelrnda φ z B w B h z Hom C w z 2 nd Y w h 1 st Y z O Nat S 1 st Y w
131 97 130 nat1st2nd φ z B w B h z Hom C w z 2 nd Y w h 1 st 1 st Y z 2 nd 1 st Y z O Nat S 1 st 1 st Y w 2 nd 1 st Y w
132 131 adantr φ z B w B h z Hom C w y B z 2 nd Y w h 1 st 1 st Y z 2 nd 1 st Y z O Nat S 1 st 1 st Y w 2 nd 1 st Y w
133 eqid Hom S = Hom S
134 97 132 52 133 114 natcl φ z B w B h z Hom C w y B z 2 nd Y w h y 1 st 1 st Y z y Hom S 1 st 1 st Y w y
135 21 adantr φ z B w B U V
136 135 ad2antrr φ z B w B h z Hom C w y B U V
137 60 ad2antrr φ z B w B h z Hom C w 1 st Y : B O Func S
138 137 112 ffvelrnd φ z B w B h z Hom C w 1 st Y z O Func S
139 1st2ndbr Rel O Func S 1 st Y z O Func S 1 st 1 st Y z O Func S 2 nd 1 st Y z
140 86 138 139 sylancr φ z B w B h z Hom C w 1 st 1 st Y z O Func S 2 nd 1 st Y z
141 52 85 140 funcf1 φ z B w B h z Hom C w 1 st 1 st Y z : B Base S
142 141 ffvelrnda φ z B w B h z Hom C w y B 1 st 1 st Y z y Base S
143 92 ad2antrr φ z B w B h z Hom C w y B U = Base S
144 142 143 eleqtrrd φ z B w B h z Hom C w y B 1 st 1 st Y z y U
145 89 adantr φ z B w B h z Hom C w 1 st 1 st Y w : B Base S
146 145 ffvelrnda φ z B w B h z Hom C w y B 1 st 1 st Y w y Base S
147 146 143 eleqtrrd φ z B w B h z Hom C w y B 1 st 1 st Y w y U
148 5 136 133 144 147 elsetchom φ z B w B h z Hom C w y B z 2 nd Y w h y 1 st 1 st Y z y Hom S 1 st 1 st Y w y z 2 nd Y w h y : 1 st 1 st Y z y 1 st 1 st Y w y
149 134 148 mpbid φ z B w B h z Hom C w y B z 2 nd Y w h y : 1 st 1 st Y z y 1 st 1 st Y w y
150 149 feqmptd φ z B w B h z Hom C w y B z 2 nd Y w h y = g 1 st 1 st Y z y z 2 nd Y w h y g
151 127 150 eqtr4d φ z B w B h z Hom C w y B g y Hom C z z 2 nd 1 st Y w y g h = z 2 nd Y w h y
152 151 mpteq2dva φ z B w B h z Hom C w y B g y Hom C z z 2 nd 1 st Y w y g h = y B z 2 nd Y w h y
153 78 adantr φ z B w B h z Hom C w V W
154 79 adantr φ z B w B h z Hom C w ran Hom 𝑓 C U
155 80 adantr φ z B w B h z Hom C w ran Hom 𝑓 Q U V
156 63 adantr φ z B w B h z Hom C w 1 st Y w O Func S
157 76 eleq2d φ z B w B h 1 st 1 st Y w z h z Hom C w
158 157 biimpar φ z B w B h z Hom C w h 1 st 1 st Y w z
159 1 2 3 4 5 6 7 8 9 10 11 110 153 154 155 156 112 18 158 yonedalem4a φ z B w B h z Hom C w 1 st Y w N z h = y B g y Hom C z z 2 nd 1 st Y w y g h
160 97 131 52 natfn φ z B w B h z Hom C w z 2 nd Y w h Fn B
161 dffn5 z 2 nd Y w h Fn B z 2 nd Y w h = y B z 2 nd Y w h y
162 160 161 sylib φ z B w B h z Hom C w z 2 nd Y w h = y B z 2 nd Y w h y
163 152 159 162 3eqtr4d φ z B w B h z Hom C w 1 st Y w N z h = z 2 nd Y w h
164 163 mpteq2dva φ z B w B h z Hom C w 1 st Y w N z h = h z Hom C w z 2 nd Y w h
165 f1of 1 st Y w N z : z Hom C w 1-1 onto 1 st Y z O Nat S 1 st Y w 1 st Y w N z : z Hom C w 1 st Y z O Nat S 1 st Y w
166 109 165 syl φ z B w B 1 st Y w N z : z Hom C w 1 st Y z O Nat S 1 st Y w
167 166 feqmptd φ z B w B 1 st Y w N z = h z Hom C w 1 st Y w N z h
168 129 feqmptd φ z B w B z 2 nd Y w = h z Hom C w z 2 nd Y w h
169 164 167 168 3eqtr4d φ z B w B 1 st Y w N z = z 2 nd Y w
170 169 f1oeq1d φ z B w B 1 st Y w N z : z Hom C w 1-1 onto 1 st Y z O Nat S 1 st Y w z 2 nd Y w : z Hom C w 1-1 onto 1 st Y z O Nat S 1 st Y w
171 109 170 mpbid φ z B w B z 2 nd Y w : z Hom C w 1-1 onto 1 st Y z O Nat S 1 st Y w
172 171 ralrimivva φ z B w B z 2 nd Y w : z Hom C w 1-1 onto 1 st Y z O Nat S 1 st Y w
173 2 75 98 isffth2 1 st Y C Full Q C Faith Q 2 nd Y 1 st Y C Func Q 2 nd Y z B w B z 2 nd Y w : z Hom C w 1-1 onto 1 st Y z O Nat S 1 st Y w
174 26 172 173 sylanbrc φ 1 st Y C Full Q C Faith Q 2 nd Y
175 df-br 1 st Y C Full Q C Faith Q 2 nd Y 1 st Y 2 nd Y C Full Q C Faith Q
176 174 175 sylib φ 1 st Y 2 nd Y C Full Q C Faith Q
177 24 176 eqeltrd φ Y C Full Q C Faith Q