Theorem ranrcl5

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

	Ref	Expression
Hypotheses	ranrcl2.l	No typesetting found for |- ( ph -> L ( F ( <. C , D >. Ran E ) X ) A ) with typecode |-
	ranrcl5.n	$$⊢N=C\mathrm{Nat}E$$
Assertion	ranrcl5	$$⊢\phi \to A\in \left(\left(L{\circ }_{\mathrm{func}}F\right)NX\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		ranrcl5.n	$$⊢N=C\mathrm{Nat}E$$
3		eqid	$$⊢\mathrm{oppCat}\left(D\mathrm{FuncCat}E\right)=\mathrm{oppCat}\left(D\mathrm{FuncCat}E\right)$$
4		eqid	$$⊢\mathrm{oppCat}\left(C\mathrm{FuncCat}E\right)=\mathrm{oppCat}\left(C\mathrm{FuncCat}E\right)$$
5	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 |-
6	3 4 5 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 |-
7		eqid	$$⊢C\mathrm{FuncCat}E=C\mathrm{FuncCat}E$$
8	7 2	fuchom	$$⊢N=\mathrm{Hom}\left(C\mathrm{FuncCat}E\right)$$
9	6 4 8	oppcuprcl5	Could not format ( ph -> A e. ( ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) N X ) ) : No typesetting found for |- ( ph -> A e. ( ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) N X ) ) with typecode |-
10	1	ranrcl4	$$⊢\phi \to L\in \left(D\mathrm{Func}E\right)$$
11		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 |-
12	10 11	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 |-
13	12	oveq1d	Could not format ( ph -> ( ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) N X ) = ( ( L o.func F ) N X ) ) : No typesetting found for |- ( ph -> ( ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) N X ) = ( ( L o.func F ) N X ) ) with typecode |-
14	9 13	eleqtrd	$$⊢\phi \to A\in \left(\left(L{\circ }_{\mathrm{func}}F\right)NX\right)$$