Theorem islan

Description: A left Kan extension is a universal pair. (Contributed by Zhi Wang, 3-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	islan	|- ( L e. ( F ( <. C , D >. Lan E ) X ) -> L e. ( K ( R UP S ) X ) )

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		id	|- ( L e. ( F ( <. C , D >. Lan E ) X ) -> L e. ( F ( <. C , D >. Lan E ) X ) )
5		lanrcl	|- ( L e. ( F ( <. C , D >. Lan E ) X ) -> ( F e. ( C Func D ) /\ X e. ( C Func E ) ) )
6	5	simpld	|- ( L e. ( F ( <. C , D >. Lan E ) X ) -> F e. ( C Func D ) )
7	5	simprd	|- ( L e. ( F ( <. C , D >. Lan E ) X ) -> X e. ( C Func E ) )
8	3	eqcomi	|- ( <. D , E >. -o.F F ) = K
9	8	a1i	|- ( L e. ( F ( <. C , D >. Lan E ) X ) -> ( <. D , E >. -o.F F ) = K )
10	1 2 6 7 9	lanval	|- ( L e. ( F ( <. C , D >. Lan E ) X ) -> ( F ( <. C , D >. Lan E ) X ) = ( K ( R UP S ) X ) )
11	4 10	eleqtrd	|- ( L e. ( F ( <. C , D >. Lan E ) X ) -> L e. ( K ( R UP S ) X ) )