Metamath Proof Explorer

Theorem lanrcl5

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

Ref Expression
Hypotheses lanrcl2.l 
|- ( ph -> L ( F ( <. C , D >. Lan E ) X ) A )
lanrcl5.n 
|- N = ( C Nat E )
Assertion lanrcl5 
|- ( ph -> A e. ( X N ( L o.func F ) ) )

Proof

Step Hyp Ref Expression
1 lanrcl2.l 
 |-  ( ph -> L ( F ( <. C , D >. Lan E ) X ) A )
2 lanrcl5.n 
 |-  N = ( C Nat E )
3 eqid 
 |-  ( D FuncCat E ) = ( D FuncCat E )
4 eqid 
 |-  ( C FuncCat E ) = ( C FuncCat E )
5 eqid 
 |-  ( <. D , E >. -o.F F ) = ( <. D , E >. -o.F F )
6 3 4 5 islan2 
 |-  ( L ( F ( <. C , D >. Lan E ) X ) A -> L ( ( <. D , E >. -o.F F ) ( ( D FuncCat E ) UP ( C FuncCat E ) ) X ) A )
7 1 6 syl 
 |-  ( ph -> L ( ( <. D , E >. -o.F F ) ( ( D FuncCat E ) UP ( C FuncCat E ) ) X ) A )
8 7 up1st2nd 
 |-  ( ph -> L ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( ( D FuncCat E ) UP ( C FuncCat E ) ) X ) A )
9 4 2 fuchom 
 |-  N = ( Hom ` ( C FuncCat E ) )
10 8 9 uprcl5 
 |-  ( ph -> A e. ( X N ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) ) )
11 1 lanrcl4 
 |-  ( ph -> L e. ( D Func E ) )
12 eqidd 
 |-  ( ph -> ( 1st ` ( <. D , E >. -o.F F ) ) = ( 1st ` ( <. D , E >. -o.F F ) ) )
13 11 12 prcof1 
 |-  ( ph -> ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) = ( L o.func F ) )
14 13 oveq2d 
 |-  ( ph -> ( X N ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) ) = ( X N ( L o.func F ) ) )
15 10 14 eleqtrd 
 |-  ( ph -> A e. ( X N ( L o.func F ) ) )