# Metamath Proof Explorer

## Theorem yonedalem4c

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}$
yonedalem4.n ${⊢}{N}=\left({f}\in \left({O}\mathrm{Func}{S}\right),{x}\in {B}⟼\left({u}\in {1}^{st}\left({f}\right)\left({x}\right)⟼\left({y}\in {B}⟼\left({g}\in \left({y}\mathrm{Hom}\left({C}\right){x}\right)⟼\left({x}{2}^{nd}\left({f}\right){y}\right)\left({g}\right)\left({u}\right)\right)\right)\right)\right)$
yonedalem4.p ${⊢}{\phi }\to {A}\in {1}^{st}\left({F}\right)\left({X}\right)$
Assertion yonedalem4c ${⊢}{\phi }\to \left({F}{N}{X}\right)\left({A}\right)\in \left({1}^{st}\left({Y}\right)\left({X}\right)\left({O}\mathrm{Nat}{S}\right){F}\right)$

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