Theorem islan2

Description: A left Kan extension is a universal pair. (Contributed by Zhi Wang, 4-Nov-2025)

	Ref	Expression
Hypotheses	islan.r	|- R = ( D FuncCat E )
	islan.s	|- S = ( C FuncCat E )
	islan.k	|- K = ( <. D , E >. -o.F F )
Assertion	islan2	|- ( L ( F ( <. C , D >. Lan E ) X ) A -> L ( K ( R UP S ) X ) A )

Proof

Step	Hyp	Ref	Expression
1		islan.r	|- R = ( D FuncCat E )
2		islan.s	|- S = ( C FuncCat E )
3		islan.k	|- K = ( <. D , E >. -o.F F )
4	1 2 3	islan	|- ( <. L , A >. e. ( F ( <. C , D >. Lan E ) X ) -> <. L , A >. e. ( K ( R UP S ) X ) )
5		df-br	|- ( L ( F ( <. C , D >. Lan E ) X ) A <-> <. L , A >. e. ( F ( <. C , D >. Lan E ) X ) )
6		df-br	|- ( L ( K ( R UP S ) X ) A <-> <. L , A >. e. ( K ( R UP S ) X ) )
7	4 5 6	3imtr4i	|- ( L ( F ( <. C , D >. Lan E ) X ) A -> L ( K ( R UP S ) X ) A )