Metamath Proof Explorer


Theorem yonedalem4c

Description: Lemma for yoneda . (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
yonedalem21.f φ F O Func S
yonedalem21.x φ X B
yonedalem4.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
yonedalem4.p φ A 1 st F X
Assertion yonedalem4c φ F N X A 1 st Y X O Nat S F

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 yonedalem21.f φ F O Func S
17 yonedalem21.x φ X B
18 yonedalem4.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 yonedalem4.p φ A 1 st F X
20 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 yonedalem4a φ F N X A = y B g y Hom C X X 2 nd F y g A
21 oveq1 y = z y Hom C X = z Hom C X
22 oveq2 y = z X 2 nd F y = X 2 nd F z
23 22 fveq1d y = z X 2 nd F y g = X 2 nd F z g
24 23 fveq1d y = z X 2 nd F y g A = X 2 nd F z g A
25 21 24 mpteq12dv y = z g y Hom C X X 2 nd F y g A = g z Hom C X X 2 nd F z g A
26 25 cbvmptv y B g y Hom C X X 2 nd F y g A = z B g z Hom C X X 2 nd F z g A
27 20 26 syl6eq φ F N X A = z B g z Hom C X X 2 nd F z g A
28 4 2 oppcbas B = Base O
29 eqid Hom O = Hom O
30 eqid Hom S = Hom S
31 relfunc Rel O Func S
32 1st2ndbr Rel O Func S F O Func S 1 st F O Func S 2 nd F
33 31 16 32 sylancr φ 1 st F O Func S 2 nd F
34 33 adantr φ z B 1 st F O Func S 2 nd F
35 17 adantr φ z B X B
36 simpr φ z B z B
37 28 29 30 34 35 36 funcf2 φ z B X 2 nd F z : X Hom O z 1 st F X Hom S 1 st F z
38 37 adantr φ z B g z Hom C X X 2 nd F z : X Hom O z 1 st F X Hom S 1 st F z
39 simpr φ z B g z Hom C X g z Hom C X
40 eqid Hom C = Hom C
41 40 4 oppchom X Hom O z = z Hom C X
42 39 41 syl6eleqr φ z B g z Hom C X g X Hom O z
43 38 42 ffvelrnd φ z B g z Hom C X X 2 nd F z g 1 st F X Hom S 1 st F z
44 15 unssbd φ U V
45 13 44 ssexd φ U V
46 45 adantr φ z B U V
47 46 adantr φ z B g z Hom C X U V
48 eqid Base S = Base S
49 28 48 33 funcf1 φ 1 st F : B Base S
50 5 45 setcbas φ U = Base S
51 50 feq3d φ 1 st F : B U 1 st F : B Base S
52 49 51 mpbird φ 1 st F : B U
53 52 17 ffvelrnd φ 1 st F X U
54 53 ad2antrr φ z B g z Hom C X 1 st F X U
55 52 ffvelrnda φ z B 1 st F z U
56 55 adantr φ z B g z Hom C X 1 st F z U
57 5 47 30 54 56 elsetchom φ z B g z Hom C X X 2 nd F z g 1 st F X Hom S 1 st F z X 2 nd F z g : 1 st F X 1 st F z
58 43 57 mpbid φ z B g z Hom C X X 2 nd F z g : 1 st F X 1 st F z
59 19 ad2antrr φ z B g z Hom C X A 1 st F X
60 58 59 ffvelrnd φ z B g z Hom C X X 2 nd F z g A 1 st F z
61 60 fmpttd φ z B g z Hom C X X 2 nd F z g A : z Hom C X 1 st F z
62 12 adantr φ z B C Cat
63 1 2 62 35 40 36 yon11 φ z B 1 st 1 st Y X z = z Hom C X
64 63 feq2d φ z B g z Hom C X X 2 nd F z g A : 1 st 1 st Y X z 1 st F z g z Hom C X X 2 nd F z g A : z Hom C X 1 st F z
65 61 64 mpbird φ z B g z Hom C X X 2 nd F z g A : 1 st 1 st Y X z 1 st F z
66 1 2 12 17 4 5 45 14 yon1cl φ 1 st Y X O Func S
67 1st2ndbr Rel O Func S 1 st Y X O Func S 1 st 1 st Y X O Func S 2 nd 1 st Y X
68 31 66 67 sylancr φ 1 st 1 st Y X O Func S 2 nd 1 st Y X
69 28 48 68 funcf1 φ 1 st 1 st Y X : B Base S
70 50 feq3d φ 1 st 1 st Y X : B U 1 st 1 st Y X : B Base S
71 69 70 mpbird φ 1 st 1 st Y X : B U
72 71 ffvelrnda φ z B 1 st 1 st Y X z U
73 5 46 30 72 55 elsetchom φ z B g z Hom C X X 2 nd F z g A 1 st 1 st Y X z Hom S 1 st F z g z Hom C X X 2 nd F z g A : 1 st 1 st Y X z 1 st F z
74 65 73 mpbird φ z B g z Hom C X X 2 nd F z g A 1 st 1 st Y X z Hom S 1 st F z
75 74 ralrimiva φ z B g z Hom C X X 2 nd F z g A 1 st 1 st Y X z Hom S 1 st F z
76 2 fvexi B V
77 mptelixpg B V z B g z Hom C X X 2 nd F z g A z B 1 st 1 st Y X z Hom S 1 st F z z B g z Hom C X X 2 nd F z g A 1 st 1 st Y X z Hom S 1 st F z
78 76 77 ax-mp z B g z Hom C X X 2 nd F z g A z B 1 st 1 st Y X z Hom S 1 st F z z B g z Hom C X X 2 nd F z g A 1 st 1 st Y X z Hom S 1 st F z
79 75 78 sylibr φ z B g z Hom C X X 2 nd F z g A z B 1 st 1 st Y X z Hom S 1 st F z
80 27 79 eqeltrd φ F N X A z B 1 st 1 st Y X z Hom S 1 st F z
81 12 adantr φ z B w B h z Hom O w C Cat
82 17 adantr φ z B w B h z Hom O w X B
83 simpr1 φ z B w B h z Hom O w z B
84 1 2 81 82 40 83 yon11 φ z B w B h z Hom O w 1 st 1 st Y X z = z Hom C X
85 84 eleq2d φ z B w B h z Hom O w k 1 st 1 st Y X z k z Hom C X
86 85 biimpa φ z B w B h z Hom O w k 1 st 1 st Y X z k z Hom C X
87 eqid comp O = comp O
88 eqid comp S = comp S
89 33 adantr φ z B w B h z Hom O w 1 st F O Func S 2 nd F
90 89 adantr φ z B w B h z Hom O w k z Hom C X 1 st F O Func S 2 nd F
91 82 adantr φ z B w B h z Hom O w k z Hom C X X B
92 83 adantr φ z B w B h z Hom O w k z Hom C X z B
93 simpr2 φ z B w B h z Hom O w w B
94 93 adantr φ z B w B h z Hom O w k z Hom C X w B
95 simpr φ z B w B h z Hom O w k z Hom C X k z Hom C X
96 95 41 syl6eleqr φ z B w B h z Hom O w k z Hom C X k X Hom O z
97 simplr3 φ z B w B h z Hom O w k z Hom C X h z Hom O w
98 28 29 87 88 90 91 92 94 96 97 funcco φ z B w B h z Hom O w k z Hom C X X 2 nd F w h X z comp O w k = z 2 nd F w h 1 st F X 1 st F z comp S 1 st F w X 2 nd F z k
99 eqid comp C = comp C
100 2 99 4 91 92 94 oppcco φ z B w B h z Hom O w k z Hom C X h X z comp O w k = k w z comp C X h
101 100 fveq2d φ z B w B h z Hom O w k z Hom C X X 2 nd F w h X z comp O w k = X 2 nd F w k w z comp C X h
102 45 adantr φ z B w B h z Hom O w U V
103 102 adantr φ z B w B h z Hom O w k z Hom C X U V
104 53 ad2antrr φ z B w B h z Hom O w k z Hom C X 1 st F X U
105 55 3ad2antr1 φ z B w B h z Hom O w 1 st F z U
106 105 adantr φ z B w B h z Hom O w k z Hom C X 1 st F z U
107 52 adantr φ z B w B h z Hom O w 1 st F : B U
108 107 93 ffvelrnd φ z B w B h z Hom O w 1 st F w U
109 108 adantr φ z B w B h z Hom O w k z Hom C X 1 st F w U
110 28 29 30 89 82 83 funcf2 φ z B w B h z Hom O w X 2 nd F z : X Hom O z 1 st F X Hom S 1 st F z
111 110 adantr φ z B w B h z Hom O w k z Hom C X X 2 nd F z : X Hom O z 1 st F X Hom S 1 st F z
112 111 96 ffvelrnd φ z B w B h z Hom O w k z Hom C X X 2 nd F z k 1 st F X Hom S 1 st F z
113 5 103 30 104 106 elsetchom φ z B w B h z Hom O w k z Hom C X X 2 nd F z k 1 st F X Hom S 1 st F z X 2 nd F z k : 1 st F X 1 st F z
114 112 113 mpbid φ z B w B h z Hom O w k z Hom C X X 2 nd F z k : 1 st F X 1 st F z
115 28 29 30 89 83 93 funcf2 φ z B w B h z Hom O w z 2 nd F w : z Hom O w 1 st F z Hom S 1 st F w
116 simpr3 φ z B w B h z Hom O w h z Hom O w
117 115 116 ffvelrnd φ z B w B h z Hom O w z 2 nd F w h 1 st F z Hom S 1 st F w
118 5 102 30 105 108 elsetchom φ z B w B h z Hom O w z 2 nd F w h 1 st F z Hom S 1 st F w z 2 nd F w h : 1 st F z 1 st F w
119 117 118 mpbid φ z B w B h z Hom O w z 2 nd F w h : 1 st F z 1 st F w
120 119 adantr φ z B w B h z Hom O w k z Hom C X z 2 nd F w h : 1 st F z 1 st F w
121 5 103 88 104 106 109 114 120 setcco φ z B w B h z Hom O w k z Hom C X z 2 nd F w h 1 st F X 1 st F z comp S 1 st F w X 2 nd F z k = z 2 nd F w h X 2 nd F z k
122 98 101 121 3eqtr3d φ z B w B h z Hom O w k z Hom C X X 2 nd F w k w z comp C X h = z 2 nd F w h X 2 nd F z k
123 122 fveq1d φ z B w B h z Hom O w k z Hom C X X 2 nd F w k w z comp C X h A = z 2 nd F w h X 2 nd F z k A
124 19 ad2antrr φ z B w B h z Hom O w k z Hom C X A 1 st F X
125 fvco3 X 2 nd F z k : 1 st F X 1 st F z A 1 st F X z 2 nd F w h X 2 nd F z k A = z 2 nd F w h X 2 nd F z k A
126 114 124 125 syl2anc φ z B w B h z Hom O w k z Hom C X z 2 nd F w h X 2 nd F z k A = z 2 nd F w h X 2 nd F z k A
127 123 126 eqtrd φ z B w B h z Hom O w k z Hom C X X 2 nd F w k w z comp C X h A = z 2 nd F w h X 2 nd F z k A
128 81 adantr φ z B w B h z Hom O w k z Hom C X C Cat
129 40 4 oppchom z Hom O w = w Hom C z
130 97 129 syl6eleq φ z B w B h z Hom O w k z Hom C X h w Hom C z
131 1 2 128 91 40 92 99 94 130 95 yon12 φ z B w B h z Hom O w k z Hom C X z 2 nd 1 st Y X w h k = k w z comp C X h
132 131 fveq2d φ z B w B h z Hom O w k z Hom C X F N X A w z 2 nd 1 st Y X w h k = F N X A w k w z comp C X h
133 13 ad2antrr φ z B w B h z Hom O w k z Hom C X V W
134 14 ad2antrr φ z B w B h z Hom O w k z Hom C X ran Hom 𝑓 C U
135 15 ad2antrr φ z B w B h z Hom O w k z Hom C X ran Hom 𝑓 Q U V
136 16 ad2antrr φ z B w B h z Hom O w k z Hom C X F O Func S
137 2 40 99 128 94 92 91 130 95 catcocl φ z B w B h z Hom O w k z Hom C X k w z comp C X h w Hom C X
138 1 2 3 4 5 6 7 8 9 10 11 128 133 134 135 136 91 18 124 94 137 yonedalem4b φ z B w B h z Hom O w k z Hom C X F N X A w k w z comp C X h = X 2 nd F w k w z comp C X h A
139 132 138 eqtrd φ z B w B h z Hom O w k z Hom C X F N X A w z 2 nd 1 st Y X w h k = X 2 nd F w k w z comp C X h A
140 1 2 3 4 5 6 7 8 9 10 11 128 133 134 135 136 91 18 124 92 95 yonedalem4b φ z B w B h z Hom O w k z Hom C X F N X A z k = X 2 nd F z k A
141 140 fveq2d φ z B w B h z Hom O w k z Hom C X z 2 nd F w h F N X A z k = z 2 nd F w h X 2 nd F z k A
142 127 139 141 3eqtr4d φ z B w B h z Hom O w k z Hom C X F N X A w z 2 nd 1 st Y X w h k = z 2 nd F w h F N X A z k
143 86 142 syldan φ z B w B h z Hom O w k 1 st 1 st Y X z F N X A w z 2 nd 1 st Y X w h k = z 2 nd F w h F N X A z k
144 143 mpteq2dva φ z B w B h z Hom O w k 1 st 1 st Y X z F N X A w z 2 nd 1 st Y X w h k = k 1 st 1 st Y X z z 2 nd F w h F N X A z k
145 fveq2 z = w F N X A z = F N X A w
146 fveq2 z = w 1 st 1 st Y X z = 1 st 1 st Y X w
147 fveq2 z = w 1 st F z = 1 st F w
148 145 146 147 feq123d z = w F N X A z : 1 st 1 st Y X z 1 st F z F N X A w : 1 st 1 st Y X w 1 st F w
149 27 fveq1d φ F N X A z = z B g z Hom C X X 2 nd F z g A z
150 ovex z Hom C X V
151 150 mptex g z Hom C X X 2 nd F z g A V
152 eqid z B g z Hom C X X 2 nd F z g A = z B g z Hom C X X 2 nd F z g A
153 152 fvmpt2 z B g z Hom C X X 2 nd F z g A V z B g z Hom C X X 2 nd F z g A z = g z Hom C X X 2 nd F z g A
154 151 153 mpan2 z B z B g z Hom C X X 2 nd F z g A z = g z Hom C X X 2 nd F z g A
155 149 154 sylan9eq φ z B F N X A z = g z Hom C X X 2 nd F z g A
156 155 feq1d φ z B F N X A z : 1 st 1 st Y X z 1 st F z g z Hom C X X 2 nd F z g A : 1 st 1 st Y X z 1 st F z
157 65 156 mpbird φ z B F N X A z : 1 st 1 st Y X z 1 st F z
158 157 ralrimiva φ z B F N X A z : 1 st 1 st Y X z 1 st F z
159 158 adantr φ z B w B h z Hom O w z B F N X A z : 1 st 1 st Y X z 1 st F z
160 148 159 93 rspcdva φ z B w B h z Hom O w F N X A w : 1 st 1 st Y X w 1 st F w
161 68 adantr φ z B w B h z Hom O w 1 st 1 st Y X O Func S 2 nd 1 st Y X
162 28 29 30 161 83 93 funcf2 φ z B w B h z Hom O w z 2 nd 1 st Y X w : z Hom O w 1 st 1 st Y X z Hom S 1 st 1 st Y X w
163 162 116 ffvelrnd φ z B w B h z Hom O w z 2 nd 1 st Y X w h 1 st 1 st Y X z Hom S 1 st 1 st Y X w
164 72 3ad2antr1 φ z B w B h z Hom O w 1 st 1 st Y X z U
165 71 adantr φ z B w B h z Hom O w 1 st 1 st Y X : B U
166 165 93 ffvelrnd φ z B w B h z Hom O w 1 st 1 st Y X w U
167 5 102 30 164 166 elsetchom φ z B w B h z Hom O w z 2 nd 1 st Y X w h 1 st 1 st Y X z Hom S 1 st 1 st Y X w z 2 nd 1 st Y X w h : 1 st 1 st Y X z 1 st 1 st Y X w
168 163 167 mpbid φ z B w B h z Hom O w z 2 nd 1 st Y X w h : 1 st 1 st Y X z 1 st 1 st Y X w
169 fcompt F N X A w : 1 st 1 st Y X w 1 st F w z 2 nd 1 st Y X w h : 1 st 1 st Y X z 1 st 1 st Y X w F N X A w z 2 nd 1 st Y X w h = k 1 st 1 st Y X z F N X A w z 2 nd 1 st Y X w h k
170 160 168 169 syl2anc φ z B w B h z Hom O w F N X A w z 2 nd 1 st Y X w h = k 1 st 1 st Y X z F N X A w z 2 nd 1 st Y X w h k
171 157 3ad2antr1 φ z B w B h z Hom O w F N X A z : 1 st 1 st Y X z 1 st F z
172 fcompt z 2 nd F w h : 1 st F z 1 st F w F N X A z : 1 st 1 st Y X z 1 st F z z 2 nd F w h F N X A z = k 1 st 1 st Y X z z 2 nd F w h F N X A z k
173 119 171 172 syl2anc φ z B w B h z Hom O w z 2 nd F w h F N X A z = k 1 st 1 st Y X z z 2 nd F w h F N X A z k
174 144 170 173 3eqtr4d φ z B w B h z Hom O w F N X A w z 2 nd 1 st Y X w h = z 2 nd F w h F N X A z
175 5 102 88 164 166 108 168 160 setcco φ z B w B h z Hom O w F N X A w 1 st 1 st Y X z 1 st 1 st Y X w comp S 1 st F w z 2 nd 1 st Y X w h = F N X A w z 2 nd 1 st Y X w h
176 5 102 88 164 105 108 171 119 setcco φ z B w B h z Hom O w z 2 nd F w h 1 st 1 st Y X z 1 st F z comp S 1 st F w F N X A z = z 2 nd F w h F N X A z
177 174 175 176 3eqtr4d φ z B w B h z Hom O w F N X A w 1 st 1 st Y X z 1 st 1 st Y X w comp S 1 st F w z 2 nd 1 st Y X w h = z 2 nd F w h 1 st 1 st Y X z 1 st F z comp S 1 st F w F N X A z
178 177 ralrimivvva φ z B w B h z Hom O w F N X A w 1 st 1 st Y X z 1 st 1 st Y X w comp S 1 st F w z 2 nd 1 st Y X w h = z 2 nd F w h 1 st 1 st Y X z 1 st F z comp S 1 st F w F N X A z
179 eqid O Nat S = O Nat S
180 179 28 29 30 88 66 16 isnat2 φ F N X A 1 st Y X O Nat S F F N X A z B 1 st 1 st Y X z Hom S 1 st F z z B w B h z Hom O w F N X A w 1 st 1 st Y X z 1 st 1 st Y X w comp S 1 st F w z 2 nd 1 st Y X w h = z 2 nd F w h 1 st 1 st Y X z 1 st F z comp S 1 st F w F N X A z
181 80 178 180 mpbir2and φ F N X A 1 st Y X O Nat S F