Theorem lanrcl4

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

	Ref	Expression
Hypothesis	lanrcl2.l	No typesetting found for |- ( ph -> L ( F ( <. C , D >. Lan E ) X ) A ) with typecode |-
Assertion	lanrcl4	$$⊢\phi \to L\in \left(D\mathrm{Func}E\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		df-br	Could not format ( L ( F ( <. C , D >. Lan E ) X ) A <-> <. L , A >. e. ( F ( <. C , D >. Lan E ) X ) ) : No typesetting found for |- ( L ( F ( <. C , D >. Lan E ) X ) A <-> <. L , A >. e. ( F ( <. C , D >. Lan E ) X ) ) with typecode |-
3	1 2	sylib	Could not format ( ph -> <. L , A >. e. ( F ( <. C , D >. Lan E ) X ) ) : No typesetting found for |- ( ph -> <. L , A >. e. ( F ( <. C , D >. Lan E ) X ) ) with typecode |-
4		eqid	$$⊢D\mathrm{FuncCat}E=D\mathrm{FuncCat}E$$
5		eqid	$$⊢C\mathrm{FuncCat}E=C\mathrm{FuncCat}E$$
6		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 |-
7	4 5 6	islan	Could not format ( <. L , A >. e. ( F ( <. C , D >. Lan E ) X ) -> <. L , A >. e. ( ( <. D , E >. -o.F F ) ( ( D FuncCat E ) UP ( C FuncCat E ) ) X ) ) : No typesetting found for |- ( <. L , A >. e. ( F ( <. C , D >. Lan E ) X ) -> <. L , A >. e. ( ( <. D , E >. -o.F F ) ( ( D FuncCat E ) UP ( C FuncCat E ) ) X ) ) with typecode |-
8	3 7	syl	Could not format ( ph -> <. L , A >. e. ( ( <. D , E >. -o.F F ) ( ( D FuncCat E ) UP ( C FuncCat E ) ) X ) ) : No typesetting found for |- ( ph -> <. L , A >. e. ( ( <. D , E >. -o.F F ) ( ( D FuncCat E ) UP ( C FuncCat E ) ) X ) ) with typecode |-
9		df-br	Could not format ( L ( ( <. D , E >. -o.F F ) ( ( D FuncCat E ) UP ( C FuncCat E ) ) X ) A <-> <. L , A >. e. ( ( <. D , E >. -o.F F ) ( ( D FuncCat E ) UP ( C FuncCat E ) ) X ) ) : No typesetting found for |- ( L ( ( <. D , E >. -o.F F ) ( ( D FuncCat E ) UP ( C FuncCat E ) ) X ) A <-> <. L , A >. e. ( ( <. D , E >. -o.F F ) ( ( D FuncCat E ) UP ( C FuncCat E ) ) X ) ) with typecode |-
10	8 9	sylibr	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 |-
11	10	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 |-
12	4	fucbas	$$⊢D\mathrm{Func}E={\mathrm{Base}}_{\left(D\mathrm{FuncCat}E\right)}$$
13	11 12	uprcl4	$$⊢\phi \to L\in \left(D\mathrm{Func}E\right)$$