Metamath Proof Explorer

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 
|- ( ph -> L ( F ( <. C , D >. Ran E ) X ) A )
Assertion ranrcl4 
|- ( ph -> L e. ( D Func E ) )

Proof

Step Hyp Ref Expression
1 ranrcl2.l 
 |-  ( ph -> L ( F ( <. C , D >. Ran E ) X ) A )
2 eqid 
 |-  ( oppCat ` ( D FuncCat E ) ) = ( oppCat ` ( D FuncCat E ) )
3 eqid 
 |-  ( oppCat ` ( C FuncCat E ) ) = ( oppCat ` ( C FuncCat E ) )
4 1 ranrcl4lem 
 |-  ( ph -> ( <. D , E >. -o.F F ) = <. ( 1st ` ( <. D , E >. -o.F F ) ) , ( 2nd ` ( <. D , E >. -o.F F ) ) >. )
5 2 3 4 1 isran2 
 |-  ( 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 )
6 eqid 
 |-  ( D FuncCat E ) = ( D FuncCat E )
7 6 fucbas 
 |-  ( D Func E ) = ( Base ` ( D FuncCat E ) )
8 5 2 7 oppcuprcl4 
 |-  ( ph -> L e. ( D Func E ) )