Theorem concl

Description: A natural transformation from a constant functor of an object maps to morphisms whose domain is the object. Therefore, the range of the second component of a cone are morphisms with a common domain. (Contributed by Zhi Wang, 13-Nov-2025)

	Ref	Expression
Hypotheses	islmd.l	$$⊢L=C{\Delta }_{\mathrm{func}}D$$
	islmd.a	$$⊢A={\mathrm{Base}}_C$$
	islmd.n	$$⊢N=D\mathrm{Nat}C$$
	islmd.b	$$⊢B={\mathrm{Base}}_D$$
	concl.k	$$⊢K=1^{st}\left(L\right)\left(X\right)$$
	concl.x	$$⊢\phi \to X\in A$$
	concl.y	$$⊢\phi \to Y\in B$$
	concl.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	concl.r	$$⊢\phi \to R\in \left(KNF\right)$$
Assertion	concl	$$⊢\phi \to R\left(Y\right)\in \left(XH{1}^{st}\left(F\right)\left(Y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		islmd.l	$$⊢L=C{\Delta }_{\mathrm{func}}D$$
2		islmd.a	$$⊢A={\mathrm{Base}}_C$$
3		islmd.n	$$⊢N=D\mathrm{Nat}C$$
4		islmd.b	$$⊢B={\mathrm{Base}}_D$$
5		concl.k	$$⊢K=1^{st}\left(L\right)\left(X\right)$$
6		concl.x	$$⊢\phi \to X\in A$$
7		concl.y	$$⊢\phi \to Y\in B$$
8		concl.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
9		concl.r	$$⊢\phi \to R\in \left(KNF\right)$$
10	3 9	nat1st2nd	$$⊢\phi \to R\in \left(⟨1^{st}\left(K\right),2^{nd}\left(K\right)⟩N⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩\right)$$
11	3 10 4 8 7	natcl	$$⊢\phi \to R\left(Y\right)\in \left(1^{st}\left(K\right)\left(Y\right)H{1}^{st}\left(F\right)\left(Y\right)\right)$$
12	3 10	natrcl3	$$⊢\phi \to 1^{st}\left(F\right)\left(D\mathrm{Func}C\right)2^{nd}\left(F\right)$$
13	12	funcrcl3	$$⊢\phi \to C\in \mathrm{Cat}$$
14	12	funcrcl2	$$⊢\phi \to D\in \mathrm{Cat}$$
15	1 13 14 2 6 5 4 7	diag11	$$⊢\phi \to 1^{st}\left(K\right)\left(Y\right)=X$$
16	15	oveq1d	$$⊢\phi \to 1^{st}\left(K\right)\left(Y\right)H{1}^{st}\left(F\right)\left(Y\right)=XH{1}^{st}\left(F\right)\left(Y\right)$$
17	11 16	eleqtrd	$$⊢\phi \to R\left(Y\right)\in \left(XH{1}^{st}\left(F\right)\left(Y\right)\right)$$