Theorem isran

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

	Ref	Expression
Hypotheses	isran.o	|- O = ( oppCat ` ( D FuncCat E ) )
	isran.p	|- P = ( oppCat ` ( C FuncCat E ) )
	isran.k	|- ( ph -> ( <. D , E >. -o.F F ) = <. J , K >. )
	isran.l	|- ( ph -> L e. ( F ( <. C , D >. Ran E ) X ) )
Assertion	isran	|- ( ph -> L e. ( <. J , tpos K >. ( O UP P ) X ) )

Proof

Step	Hyp	Ref	Expression
1		isran.o	|- O = ( oppCat ` ( D FuncCat E ) )
2		isran.p	|- P = ( oppCat ` ( C FuncCat E ) )
3		isran.k	|- ( ph -> ( <. D , E >. -o.F F ) = <. J , K >. )
4		isran.l	|- ( ph -> L e. ( F ( <. C , D >. Ran E ) X ) )
5		eqid	|- ( D FuncCat E ) = ( D FuncCat E )
6		eqid	|- ( C FuncCat E ) = ( C FuncCat E )
7		ranrcl	|- ( L e. ( F ( <. C , D >. Ran E ) X ) -> ( F e. ( C Func D ) /\ X e. ( C Func E ) ) )
8	4 7	syl	|- ( ph -> ( F e. ( C Func D ) /\ X e. ( C Func E ) ) )
9	8	simpld	|- ( ph -> F e. ( C Func D ) )
10	8	simprd	|- ( ph -> X e. ( C Func E ) )
11	5 6 9 10 3 1 2	ranval	|- ( ph -> ( F ( <. C , D >. Ran E ) X ) = ( <. J , tpos K >. ( O UP P ) X ) )
12	4 11	eleqtrd	|- ( ph -> L e. ( <. J , tpos K >. ( O UP P ) X ) )