Theorem ranval2

Description: The set of right Kan extensions is the set of universal pairs. Therefore, the explicit universal property can be recovered by oppcup2 and oppcup3lem . (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 >. )
	ranval2.f	|- ( ph -> F e. ( C Func D ) )
Assertion	ranval2	|- ( ph -> ( F ( <. C , D >. Ran E ) X ) = ( <. 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		ranval2.f	|- ( ph -> F e. ( C Func D ) )
5	3	adantr	|- ( ( ph /\ x e. ( F ( <. C , D >. Ran E ) X ) ) -> ( <. D , E >. -o.F F ) = <. J , K >. )
6		simpr	|- ( ( ph /\ x e. ( F ( <. C , D >. Ran E ) X ) ) -> x e. ( F ( <. C , D >. Ran E ) X ) )
7	1 2 5 6	isran	|- ( ( ph /\ x e. ( F ( <. C , D >. Ran E ) X ) ) -> x e. ( <. J , tpos K >. ( O UP P ) X ) )
8		simpr	|- ( ( ph /\ x e. ( <. J , tpos K >. ( O UP P ) X ) ) -> x e. ( <. J , tpos K >. ( O UP P ) X ) )
9		eqid	|- ( D FuncCat E ) = ( D FuncCat E )
10		eqid	|- ( C FuncCat E ) = ( C FuncCat E )
11	4	adantr	|- ( ( ph /\ x e. ( <. J , tpos K >. ( O UP P ) X ) ) -> F e. ( C Func D ) )
12	10	fucbas	|- ( C Func E ) = ( Base ` ( C FuncCat E ) )
13	2 12	oppcbas	|- ( C Func E ) = ( Base ` P )
14	13	uprcl	|- ( x e. ( <. J , tpos K >. ( O UP P ) X ) -> ( <. J , tpos K >. e. ( O Func P ) /\ X e. ( C Func E ) ) )
15	14	simprd	|- ( x e. ( <. J , tpos K >. ( O UP P ) X ) -> X e. ( C Func E ) )
16	15	adantl	|- ( ( ph /\ x e. ( <. J , tpos K >. ( O UP P ) X ) ) -> X e. ( C Func E ) )
17	3	adantr	|- ( ( ph /\ x e. ( <. J , tpos K >. ( O UP P ) X ) ) -> ( <. D , E >. -o.F F ) = <. J , K >. )
18	9 10 11 16 17 1 2	ranval	|- ( ( ph /\ x e. ( <. J , tpos K >. ( O UP P ) X ) ) -> ( F ( <. C , D >. Ran E ) X ) = ( <. J , tpos K >. ( O UP P ) X ) )
19	8 18	eleqtrrd	|- ( ( ph /\ x e. ( <. J , tpos K >. ( O UP P ) X ) ) -> x e. ( F ( <. C , D >. Ran E ) X ) )
20	7 19	impbida	|- ( ph -> ( x e. ( F ( <. C , D >. Ran E ) X ) <-> x e. ( <. J , tpos K >. ( O UP P ) X ) ) )
21	20	eqrdv	|- ( ph -> ( F ( <. C , D >. Ran E ) X ) = ( <. J , tpos K >. ( O UP P ) X ) )