Theorem lanrcl5

Description: The second component of a left Kan extension is a natural transformation. (Contributed by Zhi Wang, 4-Nov-2025)

	Ref	Expression
Hypotheses	lanrcl2.l	No typesetting found for |- ( ph -> L ( F ( <. C , D >. Lan E ) X ) A ) with typecode |-
	lanrcl5.n	$$⊢N=C\mathrm{Nat}E$$
Assertion	lanrcl5	$$⊢\phi \to A\in \left(XN\left(L{\circ }_{\mathrm{func}}F\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		lanrcl2.l	Could not format ( ph -> L ( F ( <. C , D >. Lan E ) X ) A ) : No typesetting found for |- ( ph -> L ( F ( <. C , D >. Lan E ) X ) A ) with typecode |-
2		lanrcl5.n	$$⊢N=C\mathrm{Nat}E$$
3		eqid	$$⊢D\mathrm{FuncCat}E=D\mathrm{FuncCat}E$$
4		eqid	$$⊢C\mathrm{FuncCat}E=C\mathrm{FuncCat}E$$
5		eqid	Could not format ( <. D , E >. -o.F F ) = ( <. D , E >. -o.F F ) : No typesetting found for |- ( <. D , E >. -o.F F ) = ( <. D , E >. -o.F F ) with typecode |-
6	3 4 5	islan2	Could not format ( L ( F ( <. C , D >. Lan E ) X ) A -> L ( ( <. D , E >. -o.F F ) ( ( D FuncCat E ) UP ( C FuncCat E ) ) X ) A ) : No typesetting found for |- ( L ( F ( <. C , D >. Lan E ) X ) A -> L ( ( <. D , E >. -o.F F ) ( ( D FuncCat E ) UP ( C FuncCat E ) ) X ) A ) with typecode |-
7	1 6	syl	Could not format ( ph -> L ( ( <. D , E >. -o.F F ) ( ( D FuncCat E ) UP ( C FuncCat E ) ) X ) A ) : No typesetting found for |- ( ph -> L ( ( <. D , E >. -o.F F ) ( ( D FuncCat E ) UP ( C FuncCat E ) ) X ) A ) with typecode |-
8	7	up1st2nd	Could not format ( ph -> L ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( ( D FuncCat E ) UP ( C FuncCat E ) ) X ) A ) : No typesetting found for |- ( ph -> L ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( ( D FuncCat E ) UP ( C FuncCat E ) ) X ) A ) with typecode |-
9	4 2	fuchom	$$⊢N=\mathrm{Hom}\left(C\mathrm{FuncCat}E\right)$$
10	8 9	uprcl5	Could not format ( ph -> A e. ( X N ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) ) ) : No typesetting found for |- ( ph -> A e. ( X N ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) ) ) with typecode |-
11	1	lanrcl4	$$⊢\phi \to L\in \left(D\mathrm{Func}E\right)$$
12		eqidd	Could not format ( ph -> ( 1st ` ( <. D , E >. -o.F F ) ) = ( 1st ` ( <. D , E >. -o.F F ) ) ) : No typesetting found for |- ( ph -> ( 1st ` ( <. D , E >. -o.F F ) ) = ( 1st ` ( <. D , E >. -o.F F ) ) ) with typecode |-
13	11 12	prcof1	Could not format ( ph -> ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) = ( L o.func F ) ) : No typesetting found for |- ( ph -> ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) = ( L o.func F ) ) with typecode |-
14	13	oveq2d	Could not format ( ph -> ( X N ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) ) = ( X N ( L o.func F ) ) ) : No typesetting found for |- ( ph -> ( X N ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) ) = ( X N ( L o.func F ) ) ) with typecode |-
15	10 14	eleqtrd	$$⊢\phi \to A\in \left(XN\left(L{\circ }_{\mathrm{func}}F\right)\right)$$