Theorem ranval3

Description: The set of right Kan extensions is the set of universal pairs. (Contributed by Zhi Wang, 26-Nov-2025)

	Ref	Expression
Hypotheses	ranval3.o	$$⊢O=\mathrm{oppCat}\left(D\mathrm{FuncCat}E\right)$$
	ranval3.p	$$⊢P=\mathrm{oppCat}\left(C\mathrm{FuncCat}E\right)$$
	ranval3.k	No typesetting found for |- K = ( <. D , E >. -o.F F ) with typecode |-
Assertion	ranval3	Could not format assertion : No typesetting found for |- ( F e. ( C Func D ) -> ( F ( <. C , D >. Ran E ) X ) = ( ( oppFunc ` K ) ( O UP P ) X ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		ranval3.o	$$⊢O=\mathrm{oppCat}\left(D\mathrm{FuncCat}E\right)$$
2		ranval3.p	$$⊢P=\mathrm{oppCat}\left(C\mathrm{FuncCat}E\right)$$
3		ranval3.k	Could not format K = ( <. D , E >. -o.F F ) : No typesetting found for |- K = ( <. D , E >. -o.F F ) with typecode |-
4		id	$$⊢F\in \left(C\mathrm{Func}D\right)\to F\in \left(C\mathrm{Func}D\right)$$
5		opex	$$⊢⟨D,E⟩\in \mathrm{V}$$
6	5	a1i	$$⊢F\in \left(C\mathrm{Func}D\right)\to ⟨D,E⟩\in \mathrm{V}$$
7	4 6	prcofelvv	Could not format ( F e. ( C Func D ) -> ( <. D , E >. -o.F F ) e. ( _V X. _V ) ) : No typesetting found for |- ( F e. ( C Func D ) -> ( <. D , E >. -o.F F ) e. ( _V X. _V ) ) with typecode |-
8		1st2nd2	Could not format ( ( <. D , E >. -o.F F ) e. ( _V X. _V ) -> ( <. D , E >. -o.F F ) = <. ( 1st ` ( <. D , E >. -o.F F ) ) , ( 2nd ` ( <. D , E >. -o.F F ) ) >. ) : No typesetting found for |- ( ( <. D , E >. -o.F F ) e. ( _V X. _V ) -> ( <. D , E >. -o.F F ) = <. ( 1st ` ( <. D , E >. -o.F F ) ) , ( 2nd ` ( <. D , E >. -o.F F ) ) >. ) with typecode |-
9	7 8	syl	Could not format ( F e. ( C Func D ) -> ( <. D , E >. -o.F F ) = <. ( 1st ` ( <. D , E >. -o.F F ) ) , ( 2nd ` ( <. D , E >. -o.F F ) ) >. ) : No typesetting found for |- ( F e. ( C Func D ) -> ( <. D , E >. -o.F F ) = <. ( 1st ` ( <. D , E >. -o.F F ) ) , ( 2nd ` ( <. D , E >. -o.F F ) ) >. ) with typecode |-
10	1 2 9 4	ranval2	Could not format ( F e. ( C Func D ) -> ( F ( <. C , D >. Ran E ) X ) = ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , tpos ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( O UP P ) X ) ) : No typesetting found for |- ( F e. ( C Func D ) -> ( F ( <. C , D >. Ran E ) X ) = ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , tpos ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( O UP P ) X ) ) with typecode |-
11		eqid	$$⊢C\mathrm{FuncCat}E=C\mathrm{FuncCat}E$$
12	11	fucbas	$$⊢C\mathrm{Func}E={\mathrm{Base}}_{\left(C\mathrm{FuncCat}E\right)}$$
13	2 12	oppcbas	$$⊢C\mathrm{Func}E={\mathrm{Base}}_P$$
14	13	uprcl	Could not format ( x e. ( ( oppFunc ` K ) ( O UP P ) X ) -> ( ( oppFunc ` K ) e. ( O Func P ) /\ X e. ( C Func E ) ) ) : No typesetting found for |- ( x e. ( ( oppFunc ` K ) ( O UP P ) X ) -> ( ( oppFunc ` K ) e. ( O Func P ) /\ X e. ( C Func E ) ) ) with typecode |-
15	14	simprd	Could not format ( x e. ( ( oppFunc ` K ) ( O UP P ) X ) -> X e. ( C Func E ) ) : No typesetting found for |- ( x e. ( ( oppFunc ` K ) ( O UP P ) X ) -> X e. ( C Func E ) ) with typecode |-
16	15	adantl	Could not format ( ( F e. ( C Func D ) /\ x e. ( ( oppFunc ` K ) ( O UP P ) X ) ) -> X e. ( C Func E ) ) : No typesetting found for |- ( ( F e. ( C Func D ) /\ x e. ( ( oppFunc ` K ) ( O UP P ) X ) ) -> X e. ( C Func E ) ) with typecode |-
17	13	uprcl	Could not format ( x e. ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , tpos ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( O UP P ) X ) -> ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , tpos ( 2nd ` ( <. D , E >. -o.F F ) ) >. e. ( O Func P ) /\ X e. ( C Func E ) ) ) : No typesetting found for |- ( x e. ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , tpos ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( O UP P ) X ) -> ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , tpos ( 2nd ` ( <. D , E >. -o.F F ) ) >. e. ( O Func P ) /\ X e. ( C Func E ) ) ) with typecode |-
18	17	simprd	Could not format ( x e. ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , tpos ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( O UP P ) X ) -> X e. ( C Func E ) ) : No typesetting found for |- ( x e. ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , tpos ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( O UP P ) X ) -> X e. ( C Func E ) ) with typecode |-
19	18	adantl	Could not format ( ( F e. ( C Func D ) /\ x e. ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , tpos ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( O UP P ) X ) ) -> X e. ( C Func E ) ) : No typesetting found for |- ( ( F e. ( C Func D ) /\ x e. ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , tpos ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( O UP P ) X ) ) -> X e. ( C Func E ) ) with typecode |-
20		eqid	$$⊢D\mathrm{FuncCat}E=D\mathrm{FuncCat}E$$
21		funcrcl	$$⊢X\in \left(C\mathrm{Func}E\right)\to \left(C\in \mathrm{Cat}\wedge E\in \mathrm{Cat}\right)$$
22	21	simprd	$$⊢X\in \left(C\mathrm{Func}E\right)\to E\in \mathrm{Cat}$$
23	22	adantl	$$⊢\left(F\in \left(C\mathrm{Func}D\right)\wedge X\in \left(C\mathrm{Func}E\right)\right)\to E\in \mathrm{Cat}$$
24		simpl	$$⊢\left(F\in \left(C\mathrm{Func}D\right)\wedge X\in \left(C\mathrm{Func}E\right)\right)\to F\in \left(C\mathrm{Func}D\right)$$
25	20 23 11 24	prcoffunca	Could not format ( ( F e. ( C Func D ) /\ X e. ( C Func E ) ) -> ( <. D , E >. -o.F F ) e. ( ( D FuncCat E ) Func ( C FuncCat E ) ) ) : No typesetting found for |- ( ( F e. ( C Func D ) /\ X e. ( C Func E ) ) -> ( <. D , E >. -o.F F ) e. ( ( D FuncCat E ) Func ( C FuncCat E ) ) ) with typecode |-
26	3	fveq2i	Could not format ( oppFunc ` K ) = ( oppFunc ` ( <. D , E >. -o.F F ) ) : No typesetting found for |- ( oppFunc ` K ) = ( oppFunc ` ( <. D , E >. -o.F F ) ) with typecode |-
27		oppfval2	Could not format ( ( <. D , E >. -o.F F ) e. ( ( D FuncCat E ) Func ( C FuncCat E ) ) -> ( oppFunc ` ( <. D , E >. -o.F F ) ) = <. ( 1st ` ( <. D , E >. -o.F F ) ) , tpos ( 2nd ` ( <. D , E >. -o.F F ) ) >. ) : No typesetting found for |- ( ( <. D , E >. -o.F F ) e. ( ( D FuncCat E ) Func ( C FuncCat E ) ) -> ( oppFunc ` ( <. D , E >. -o.F F ) ) = <. ( 1st ` ( <. D , E >. -o.F F ) ) , tpos ( 2nd ` ( <. D , E >. -o.F F ) ) >. ) with typecode |-
28	26 27	eqtrid	Could not format ( ( <. D , E >. -o.F F ) e. ( ( D FuncCat E ) Func ( C FuncCat E ) ) -> ( oppFunc ` K ) = <. ( 1st ` ( <. D , E >. -o.F F ) ) , tpos ( 2nd ` ( <. D , E >. -o.F F ) ) >. ) : No typesetting found for |- ( ( <. D , E >. -o.F F ) e. ( ( D FuncCat E ) Func ( C FuncCat E ) ) -> ( oppFunc ` K ) = <. ( 1st ` ( <. D , E >. -o.F F ) ) , tpos ( 2nd ` ( <. D , E >. -o.F F ) ) >. ) with typecode |-
29	25 28	syl	Could not format ( ( F e. ( C Func D ) /\ X e. ( C Func E ) ) -> ( oppFunc ` K ) = <. ( 1st ` ( <. D , E >. -o.F F ) ) , tpos ( 2nd ` ( <. D , E >. -o.F F ) ) >. ) : No typesetting found for |- ( ( F e. ( C Func D ) /\ X e. ( C Func E ) ) -> ( oppFunc ` K ) = <. ( 1st ` ( <. D , E >. -o.F F ) ) , tpos ( 2nd ` ( <. D , E >. -o.F F ) ) >. ) with typecode |-
30	29	oveq1d	Could not format ( ( F e. ( C Func D ) /\ X e. ( C Func E ) ) -> ( ( oppFunc ` K ) ( O UP P ) X ) = ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , tpos ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( O UP P ) X ) ) : No typesetting found for |- ( ( F e. ( C Func D ) /\ X e. ( C Func E ) ) -> ( ( oppFunc ` K ) ( O UP P ) X ) = ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , tpos ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( O UP P ) X ) ) with typecode |-
31	30	eleq2d	Could not format ( ( F e. ( C Func D ) /\ X e. ( C Func E ) ) -> ( x e. ( ( oppFunc ` K ) ( O UP P ) X ) <-> x e. ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , tpos ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( O UP P ) X ) ) ) : No typesetting found for |- ( ( F e. ( C Func D ) /\ X e. ( C Func E ) ) -> ( x e. ( ( oppFunc ` K ) ( O UP P ) X ) <-> x e. ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , tpos ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( O UP P ) X ) ) ) with typecode |-
32	16 19 31	bibiad	Could not format ( F e. ( C Func D ) -> ( x e. ( ( oppFunc ` K ) ( O UP P ) X ) <-> x e. ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , tpos ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( O UP P ) X ) ) ) : No typesetting found for |- ( F e. ( C Func D ) -> ( x e. ( ( oppFunc ` K ) ( O UP P ) X ) <-> x e. ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , tpos ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( O UP P ) X ) ) ) with typecode |-
33	32	eqrdv	Could not format ( F e. ( C Func D ) -> ( ( oppFunc ` K ) ( O UP P ) X ) = ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , tpos ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( O UP P ) X ) ) : No typesetting found for |- ( F e. ( C Func D ) -> ( ( oppFunc ` K ) ( O UP P ) X ) = ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , tpos ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( O UP P ) X ) ) with typecode |-
34	10 33	eqtr4d	Could not format ( F e. ( C Func D ) -> ( F ( <. C , D >. Ran E ) X ) = ( ( oppFunc ` K ) ( O UP P ) X ) ) : No typesetting found for |- ( F e. ( C Func D ) -> ( F ( <. C , D >. Ran E ) X ) = ( ( oppFunc ` K ) ( O UP P ) X ) ) with typecode |-