Theorem ranrcl4

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

	Ref	Expression
Hypothesis	ranrcl2.l	No typesetting found for |- ( ph -> L ( F ( <. C , D >. Ran E ) X ) A ) with typecode |-
Assertion	ranrcl4	$$⊢\phi \to L\in \left(D\mathrm{Func}E\right)$$

Proof

Step	Hyp	Ref	Expression
1		ranrcl2.l	Could not format ( ph -> L ( F ( <. C , D >. Ran E ) X ) A ) : No typesetting found for |- ( ph -> L ( F ( <. C , D >. Ran E ) X ) A ) with typecode |-
2		eqid	$$⊢\mathrm{oppCat}\left(D\mathrm{FuncCat}E\right)=\mathrm{oppCat}\left(D\mathrm{FuncCat}E\right)$$
3		eqid	$$⊢\mathrm{oppCat}\left(C\mathrm{FuncCat}E\right)=\mathrm{oppCat}\left(C\mathrm{FuncCat}E\right)$$
4	1	ranrcl4lem	Could not format ( ph -> ( <. D , E >. -o.F F ) = <. ( 1st ` ( <. D , E >. -o.F F ) ) , ( 2nd ` ( <. D , E >. -o.F F ) ) >. ) : No typesetting found for |- ( ph -> ( <. D , E >. -o.F F ) = <. ( 1st ` ( <. D , E >. -o.F F ) ) , ( 2nd ` ( <. D , E >. -o.F F ) ) >. ) with typecode |-
5	2 3 4 1	isran2	Could not format ( ph -> L ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , tpos ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( ( oppCat ` ( D FuncCat E ) ) UP ( oppCat ` ( C FuncCat E ) ) ) X ) A ) : No typesetting found for |- ( ph -> L ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , tpos ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( ( oppCat ` ( D FuncCat E ) ) UP ( oppCat ` ( C FuncCat E ) ) ) X ) A ) with typecode |-
6		eqid	$$⊢D\mathrm{FuncCat}E=D\mathrm{FuncCat}E$$
7	6	fucbas	$$⊢D\mathrm{Func}E={\mathrm{Base}}_{\left(D\mathrm{FuncCat}E\right)}$$
8	5 2 7	oppcuprcl4	$$⊢\phi \to L\in \left(D\mathrm{Func}E\right)$$