Theorem isran2

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 >. )
	isran2.l	|- ( ph -> L ( F ( <. C , D >. Ran E ) X ) A )
Assertion	isran2	|- ( ph -> L ( <. J , tpos K >. ( O UP P ) X ) A )

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		isran2.l	|- ( ph -> L ( F ( <. C , D >. Ran E ) X ) A )
5		df-br	|- ( L ( F ( <. C , D >. Ran E ) X ) A <-> <. L , A >. e. ( F ( <. C , D >. Ran E ) X ) )
6	4 5	sylib	|- ( ph -> <. L , A >. e. ( F ( <. C , D >. Ran E ) X ) )
7	1 2 3 6	isran	|- ( ph -> <. L , A >. e. ( <. J , tpos K >. ( O UP P ) X ) )
8		df-br	|- ( L ( <. J , tpos K >. ( O UP P ) X ) A <-> <. L , A >. e. ( <. J , tpos K >. ( O UP P ) X ) )
9	7 8	sylibr	|- ( ph -> L ( <. J , tpos K >. ( O UP P ) X ) A )