Metamath Proof Explorer

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 
|- ( ph -> L ( F ( <. C , D >. Ran E ) X ) A )
ranrcl5.n 
|- N = ( C Nat E )
Assertion ranrcl5 
|- ( ph -> A e. ( ( L o.func F ) N X ) )

Proof

Step Hyp Ref Expression
1 ranrcl2.l 
 |-  ( ph -> L ( F ( <. C , D >. Ran E ) X ) A )
2 ranrcl5.n 
 |-  N = ( C Nat E )
3 eqid 
 |-  ( oppCat ` ( D FuncCat E ) ) = ( oppCat ` ( D FuncCat E ) )
4 eqid 
 |-  ( oppCat ` ( C FuncCat E ) ) = ( oppCat ` ( C FuncCat E ) )
5 1 ranrcl4lem 
 |-  ( ph -> ( <. D , E >. -o.F F ) = <. ( 1st ` ( <. D , E >. -o.F F ) ) , ( 2nd ` ( <. D , E >. -o.F F ) ) >. )
6 3 4 5 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 )
7 eqid 
 |-  ( C FuncCat E ) = ( C FuncCat E )
8 7 2 fuchom 
 |-  N = ( Hom ` ( C FuncCat E ) )
9 6 4 8 oppcuprcl5 
 |-  ( ph -> A e. ( ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) N X ) )
10 1 ranrcl4 
 |-  ( ph -> L e. ( D Func E ) )
11 eqidd 
 |-  ( ph -> ( 1st ` ( <. D , E >. -o.F F ) ) = ( 1st ` ( <. D , E >. -o.F F ) ) )
12 10 11 prcof1 
 |-  ( ph -> ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) = ( L o.func F ) )
13 12 oveq1d 
 |-  ( ph -> ( ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) N X ) = ( ( L o.func F ) N X ) )
14 9 13 eleqtrd 
 |-  ( ph -> A e. ( ( L o.func F ) N X ) )