# Metamath Proof Explorer

## Theorem yonedalem3a

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

Ref Expression
Hypotheses yoneda.y ${⊢}{Y}=\mathrm{Yon}\left({C}\right)$
yoneda.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
yoneda.1
yoneda.o ${⊢}{O}=\mathrm{oppCat}\left({C}\right)$
yoneda.s ${⊢}{S}=\mathrm{SetCat}\left({U}\right)$
yoneda.t ${⊢}{T}=\mathrm{SetCat}\left({V}\right)$
yoneda.q ${⊢}{Q}={O}\mathrm{FuncCat}{S}$
yoneda.h ${⊢}{H}={Hom}_{F}\left({Q}\right)$
yoneda.r ${⊢}{R}=\left({Q}{×}_{c}{O}\right)\mathrm{FuncCat}{T}$
yoneda.e ${⊢}{E}={O}{eval}_{F}{S}$
yoneda.z ${⊢}{Z}={H}{\circ }_{\mathrm{func}}\left(\left(⟨{1}^{st}\left({Y}\right),tpos{2}^{nd}\left({Y}\right)⟩{\circ }_{\mathrm{func}}\left({Q}{{2}^{nd}}_{F}{O}\right)\right){⟨,⟩}_{F}\left({Q}{{1}^{st}}_{F}{O}\right)\right)$
yoneda.c ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
yoneda.w ${⊢}{\phi }\to {V}\in {W}$
yoneda.u ${⊢}{\phi }\to \mathrm{ran}{\mathrm{Hom}}_{𝑓}\left({C}\right)\subseteq {U}$
yoneda.v ${⊢}{\phi }\to \mathrm{ran}{\mathrm{Hom}}_{𝑓}\left({Q}\right)\cup {U}\subseteq {V}$
yonedalem21.f ${⊢}{\phi }\to {F}\in \left({O}\mathrm{Func}{S}\right)$
yonedalem21.x ${⊢}{\phi }\to {X}\in {B}$
yonedalem3a.m
Assertion yonedalem3a

### Proof

Step Hyp Ref Expression
1 yoneda.y ${⊢}{Y}=\mathrm{Yon}\left({C}\right)$
2 yoneda.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
3 yoneda.1
4 yoneda.o ${⊢}{O}=\mathrm{oppCat}\left({C}\right)$
5 yoneda.s ${⊢}{S}=\mathrm{SetCat}\left({U}\right)$
6 yoneda.t ${⊢}{T}=\mathrm{SetCat}\left({V}\right)$
7 yoneda.q ${⊢}{Q}={O}\mathrm{FuncCat}{S}$
8 yoneda.h ${⊢}{H}={Hom}_{F}\left({Q}\right)$
9 yoneda.r ${⊢}{R}=\left({Q}{×}_{c}{O}\right)\mathrm{FuncCat}{T}$
10 yoneda.e ${⊢}{E}={O}{eval}_{F}{S}$
11 yoneda.z ${⊢}{Z}={H}{\circ }_{\mathrm{func}}\left(\left(⟨{1}^{st}\left({Y}\right),tpos{2}^{nd}\left({Y}\right)⟩{\circ }_{\mathrm{func}}\left({Q}{{2}^{nd}}_{F}{O}\right)\right){⟨,⟩}_{F}\left({Q}{{1}^{st}}_{F}{O}\right)\right)$
12 yoneda.c ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
13 yoneda.w ${⊢}{\phi }\to {V}\in {W}$
14 yoneda.u ${⊢}{\phi }\to \mathrm{ran}{\mathrm{Hom}}_{𝑓}\left({C}\right)\subseteq {U}$
15 yoneda.v ${⊢}{\phi }\to \mathrm{ran}{\mathrm{Hom}}_{𝑓}\left({Q}\right)\cup {U}\subseteq {V}$
16 yonedalem21.f ${⊢}{\phi }\to {F}\in \left({O}\mathrm{Func}{S}\right)$
17 yonedalem21.x ${⊢}{\phi }\to {X}\in {B}$
18 yonedalem3a.m
19 simpr ${⊢}\left({f}={F}\wedge {x}={X}\right)\to {x}={X}$
20 19 fveq2d ${⊢}\left({f}={F}\wedge {x}={X}\right)\to {1}^{st}\left({Y}\right)\left({x}\right)={1}^{st}\left({Y}\right)\left({X}\right)$
21 simpl ${⊢}\left({f}={F}\wedge {x}={X}\right)\to {f}={F}$
22 20 21 oveq12d ${⊢}\left({f}={F}\wedge {x}={X}\right)\to {1}^{st}\left({Y}\right)\left({x}\right)\left({O}\mathrm{Nat}{S}\right){f}={1}^{st}\left({Y}\right)\left({X}\right)\left({O}\mathrm{Nat}{S}\right){F}$
23 19 fveq2d ${⊢}\left({f}={F}\wedge {x}={X}\right)\to {a}\left({x}\right)={a}\left({X}\right)$
24 19 fveq2d
25 23 24 fveq12d
26 22 25 mpteq12dv
27 ovex ${⊢}{1}^{st}\left({Y}\right)\left({X}\right)\left({O}\mathrm{Nat}{S}\right){F}\in \mathrm{V}$
28 27 mptex
29 26 18 28 ovmpoa
30 16 17 29 syl2anc
31 eqid ${⊢}{O}\mathrm{Nat}{S}={O}\mathrm{Nat}{S}$
32 simpr ${⊢}\left({\phi }\wedge {a}\in \left({1}^{st}\left({Y}\right)\left({X}\right)\left({O}\mathrm{Nat}{S}\right){F}\right)\right)\to {a}\in \left({1}^{st}\left({Y}\right)\left({X}\right)\left({O}\mathrm{Nat}{S}\right){F}\right)$
33 31 32 nat1st2nd ${⊢}\left({\phi }\wedge {a}\in \left({1}^{st}\left({Y}\right)\left({X}\right)\left({O}\mathrm{Nat}{S}\right){F}\right)\right)\to {a}\in \left(⟨{1}^{st}\left({1}^{st}\left({Y}\right)\left({X}\right)\right),{2}^{nd}\left({1}^{st}\left({Y}\right)\left({X}\right)\right)⟩\left({O}\mathrm{Nat}{S}\right)⟨{1}^{st}\left({F}\right),{2}^{nd}\left({F}\right)⟩\right)$
34 4 2 oppcbas ${⊢}{B}={\mathrm{Base}}_{{O}}$
35 eqid ${⊢}\mathrm{Hom}\left({S}\right)=\mathrm{Hom}\left({S}\right)$
36 17 adantr ${⊢}\left({\phi }\wedge {a}\in \left({1}^{st}\left({Y}\right)\left({X}\right)\left({O}\mathrm{Nat}{S}\right){F}\right)\right)\to {X}\in {B}$
37 31 33 34 35 36 natcl ${⊢}\left({\phi }\wedge {a}\in \left({1}^{st}\left({Y}\right)\left({X}\right)\left({O}\mathrm{Nat}{S}\right){F}\right)\right)\to {a}\left({X}\right)\in \left({1}^{st}\left({1}^{st}\left({Y}\right)\left({X}\right)\right)\left({X}\right)\mathrm{Hom}\left({S}\right){1}^{st}\left({F}\right)\left({X}\right)\right)$
38 15 unssbd ${⊢}{\phi }\to {U}\subseteq {V}$
39 13 38 ssexd ${⊢}{\phi }\to {U}\in \mathrm{V}$
40 39 adantr ${⊢}\left({\phi }\wedge {a}\in \left({1}^{st}\left({Y}\right)\left({X}\right)\left({O}\mathrm{Nat}{S}\right){F}\right)\right)\to {U}\in \mathrm{V}$
41 eqid ${⊢}{\mathrm{Base}}_{{S}}={\mathrm{Base}}_{{S}}$
42 relfunc ${⊢}\mathrm{Rel}\left({O}\mathrm{Func}{S}\right)$
43 1 2 12 17 4 5 39 14 yon1cl ${⊢}{\phi }\to {1}^{st}\left({Y}\right)\left({X}\right)\in \left({O}\mathrm{Func}{S}\right)$
44 1st2ndbr ${⊢}\left(\mathrm{Rel}\left({O}\mathrm{Func}{S}\right)\wedge {1}^{st}\left({Y}\right)\left({X}\right)\in \left({O}\mathrm{Func}{S}\right)\right)\to {1}^{st}\left({1}^{st}\left({Y}\right)\left({X}\right)\right)\left({O}\mathrm{Func}{S}\right){2}^{nd}\left({1}^{st}\left({Y}\right)\left({X}\right)\right)$
45 42 43 44 sylancr ${⊢}{\phi }\to {1}^{st}\left({1}^{st}\left({Y}\right)\left({X}\right)\right)\left({O}\mathrm{Func}{S}\right){2}^{nd}\left({1}^{st}\left({Y}\right)\left({X}\right)\right)$
46 34 41 45 funcf1 ${⊢}{\phi }\to {1}^{st}\left({1}^{st}\left({Y}\right)\left({X}\right)\right):{B}⟶{\mathrm{Base}}_{{S}}$
47 46 17 ffvelrnd ${⊢}{\phi }\to {1}^{st}\left({1}^{st}\left({Y}\right)\left({X}\right)\right)\left({X}\right)\in {\mathrm{Base}}_{{S}}$
48 5 39 setcbas ${⊢}{\phi }\to {U}={\mathrm{Base}}_{{S}}$
49 47 48 eleqtrrd ${⊢}{\phi }\to {1}^{st}\left({1}^{st}\left({Y}\right)\left({X}\right)\right)\left({X}\right)\in {U}$
50 49 adantr ${⊢}\left({\phi }\wedge {a}\in \left({1}^{st}\left({Y}\right)\left({X}\right)\left({O}\mathrm{Nat}{S}\right){F}\right)\right)\to {1}^{st}\left({1}^{st}\left({Y}\right)\left({X}\right)\right)\left({X}\right)\in {U}$
51 1st2ndbr ${⊢}\left(\mathrm{Rel}\left({O}\mathrm{Func}{S}\right)\wedge {F}\in \left({O}\mathrm{Func}{S}\right)\right)\to {1}^{st}\left({F}\right)\left({O}\mathrm{Func}{S}\right){2}^{nd}\left({F}\right)$
52 42 16 51 sylancr ${⊢}{\phi }\to {1}^{st}\left({F}\right)\left({O}\mathrm{Func}{S}\right){2}^{nd}\left({F}\right)$
53 34 41 52 funcf1 ${⊢}{\phi }\to {1}^{st}\left({F}\right):{B}⟶{\mathrm{Base}}_{{S}}$
54 53 17 ffvelrnd ${⊢}{\phi }\to {1}^{st}\left({F}\right)\left({X}\right)\in {\mathrm{Base}}_{{S}}$
55 54 48 eleqtrrd ${⊢}{\phi }\to {1}^{st}\left({F}\right)\left({X}\right)\in {U}$
56 55 adantr ${⊢}\left({\phi }\wedge {a}\in \left({1}^{st}\left({Y}\right)\left({X}\right)\left({O}\mathrm{Nat}{S}\right){F}\right)\right)\to {1}^{st}\left({F}\right)\left({X}\right)\in {U}$
57 5 40 35 50 56 elsetchom ${⊢}\left({\phi }\wedge {a}\in \left({1}^{st}\left({Y}\right)\left({X}\right)\left({O}\mathrm{Nat}{S}\right){F}\right)\right)\to \left({a}\left({X}\right)\in \left({1}^{st}\left({1}^{st}\left({Y}\right)\left({X}\right)\right)\left({X}\right)\mathrm{Hom}\left({S}\right){1}^{st}\left({F}\right)\left({X}\right)\right)↔{a}\left({X}\right):{1}^{st}\left({1}^{st}\left({Y}\right)\left({X}\right)\right)\left({X}\right)⟶{1}^{st}\left({F}\right)\left({X}\right)\right)$
58 37 57 mpbid ${⊢}\left({\phi }\wedge {a}\in \left({1}^{st}\left({Y}\right)\left({X}\right)\left({O}\mathrm{Nat}{S}\right){F}\right)\right)\to {a}\left({X}\right):{1}^{st}\left({1}^{st}\left({Y}\right)\left({X}\right)\right)\left({X}\right)⟶{1}^{st}\left({F}\right)\left({X}\right)$
59 eqid ${⊢}\mathrm{Hom}\left({C}\right)=\mathrm{Hom}\left({C}\right)$
60 2 59 3 12 17 catidcl
61 1 2 12 17 59 17 yon11 ${⊢}{\phi }\to {1}^{st}\left({1}^{st}\left({Y}\right)\left({X}\right)\right)\left({X}\right)={X}\mathrm{Hom}\left({C}\right){X}$
62 60 61 eleqtrrd
63 62 adantr
64 58 63 ffvelrnd
65 64 fmpttd
66 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 yonedalem21 ${⊢}{\phi }\to {F}{1}^{st}\left({Z}\right){X}={1}^{st}\left({Y}\right)\left({X}\right)\left({O}\mathrm{Nat}{S}\right){F}$
67 4 oppccat ${⊢}{C}\in \mathrm{Cat}\to {O}\in \mathrm{Cat}$
68 12 67 syl ${⊢}{\phi }\to {O}\in \mathrm{Cat}$
69 5 setccat ${⊢}{U}\in \mathrm{V}\to {S}\in \mathrm{Cat}$
70 39 69 syl ${⊢}{\phi }\to {S}\in \mathrm{Cat}$
71 10 68 70 34 16 17 evlf1 ${⊢}{\phi }\to {F}{1}^{st}\left({E}\right){X}={1}^{st}\left({F}\right)\left({X}\right)$
72 30 66 71 feq123d
73 65 72 mpbird ${⊢}{\phi }\to \left({F}{M}{X}\right):{F}{1}^{st}\left({Z}\right){X}⟶{F}{1}^{st}\left({E}\right){X}$
74 30 73 jca