Theorem lanrcl2

Description: Reverse closure for left Kan extensions. (Contributed by Zhi Wang, 4-Nov-2025)

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

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		lanrcl	|- ( <. L , A >. e. ( F ( <. C , D >. Lan E ) X ) -> ( F e. ( C Func D ) /\ X e. ( C Func E ) ) )
5	3 4	syl	|- ( ph -> ( F e. ( C Func D ) /\ X e. ( C Func E ) ) )
6	5	simpld	|- ( ph -> F e. ( C Func D ) )