Metamath Proof Explorer

Theorem lanrcl4

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

Ref Expression
Hypothesis lanrcl2.l 
|- ( ph -> L ( F ( <. C , D >. Lan E ) X ) A )
Assertion lanrcl4 
|- ( ph -> L e. ( D Func E ) )

Proof

Step Hyp Ref Expression
1 lanrcl2.l 
 |-  ( ph -> L ( F ( <. C , D >. Lan E ) X ) A )
2 df-br 
 |-  ( L ( F ( <. C , D >. Lan E ) X ) A <-> <. L , A >. e. ( F ( <. C , D >. Lan E ) X ) )
3 1 2 sylib 
 |-  ( ph -> <. L , A >. e. ( F ( <. C , D >. Lan E ) X ) )
4 eqid 
 |-  ( D FuncCat E ) = ( D FuncCat E )
5 eqid 
 |-  ( C FuncCat E ) = ( C FuncCat E )
6 eqid 
 |-  ( <. D , E >. -o.F F ) = ( <. D , E >. -o.F F )
7 4 5 6 islan 
 |-  ( <. L , A >. e. ( F ( <. C , D >. Lan E ) X ) -> <. L , A >. e. ( ( <. D , E >. -o.F F ) ( ( D FuncCat E ) UP ( C FuncCat E ) ) X ) )
8 3 7 syl 
 |-  ( ph -> <. L , A >. e. ( ( <. D , E >. -o.F F ) ( ( D FuncCat E ) UP ( C FuncCat E ) ) X ) )
9 df-br 
 |-  ( L ( ( <. D , E >. -o.F F ) ( ( D FuncCat E ) UP ( C FuncCat E ) ) X ) A <-> <. L , A >. e. ( ( <. D , E >. -o.F F ) ( ( D FuncCat E ) UP ( C FuncCat E ) ) X ) )
10 8 9 sylibr 
 |-  ( ph -> L ( ( <. D , E >. -o.F F ) ( ( D FuncCat E ) UP ( C FuncCat E ) ) X ) A )
11 10 up1st2nd 
 |-  ( ph -> L ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( ( D FuncCat E ) UP ( C FuncCat E ) ) X ) A )
12 4 fucbas 
 |-  ( D Func E ) = ( Base ` ( D FuncCat E ) )
13 11 12 uprcl4 
 |-  ( ph -> L e. ( D Func E ) )