Theorem ranfval

Description: Value of the function generating the set of right Kan extensions. (Contributed by Zhi Wang, 4-Nov-2025)

	Ref	Expression
Hypotheses	lanfval.r	|- R = ( D FuncCat E )
	lanfval.s	|- S = ( C FuncCat E )
	lanfval.c	|- ( ph -> C e. U )
	lanfval.d	|- ( ph -> D e. V )
	lanfval.e	|- ( ph -> E e. W )
	ranfval.o	|- O = ( oppCat ` R )
	ranfval.p	|- P = ( oppCat ` S )
Assertion	ranfval	|- ( ph -> ( <. C , D >. Ran E ) = ( f e. ( C Func D ) , x e. ( C Func E ) |-> ( ( oppFunc ` ( <. D , E >. -o.F f ) ) ( O UP P ) x ) ) )

Proof

Step	Hyp	Ref	Expression
1		lanfval.r	|- R = ( D FuncCat E )
2		lanfval.s	|- S = ( C FuncCat E )
3		lanfval.c	|- ( ph -> C e. U )
4		lanfval.d	|- ( ph -> D e. V )
5		lanfval.e	|- ( ph -> E e. W )
6		ranfval.o	|- O = ( oppCat ` R )
7		ranfval.p	|- P = ( oppCat ` S )
8		df-ran	|- Ran = ( p e. ( _V X. _V ) , e e. _V |-> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( oppFunc ` ( <. d , e >. -o.F f ) ) ( ( oppCat ` ( d FuncCat e ) ) UP ( oppCat ` ( c FuncCat e ) ) ) x ) ) )
9	8	a1i	|- ( ph -> Ran = ( p e. ( _V X. _V ) , e e. _V |-> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( oppFunc ` ( <. d , e >. -o.F f ) ) ( ( oppCat ` ( d FuncCat e ) ) UP ( oppCat ` ( c FuncCat e ) ) ) x ) ) ) )
10		fvexd	|- ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) -> ( 1st ` p ) e. _V )
11		simprl	|- ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) -> p = <. C , D >. )
12	11	fveq2d	|- ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) -> ( 1st ` p ) = ( 1st ` <. C , D >. ) )
13		op1stg	|- ( ( C e. U /\ D e. V ) -> ( 1st ` <. C , D >. ) = C )
14	3 4 13	syl2anc	|- ( ph -> ( 1st ` <. C , D >. ) = C )
15	14	adantr	|- ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) -> ( 1st ` <. C , D >. ) = C )
16	12 15	eqtrd	|- ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) -> ( 1st ` p ) = C )
17		fvexd	|- ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) -> ( 2nd ` p ) e. _V )
18		simplrl	|- ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) -> p = <. C , D >. )
19	18	fveq2d	|- ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) -> ( 2nd ` p ) = ( 2nd ` <. C , D >. ) )
20		op2ndg	|- ( ( C e. U /\ D e. V ) -> ( 2nd ` <. C , D >. ) = D )
21	3 4 20	syl2anc	|- ( ph -> ( 2nd ` <. C , D >. ) = D )
22	21	ad2antrr	|- ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) -> ( 2nd ` <. C , D >. ) = D )
23	19 22	eqtrd	|- ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) -> ( 2nd ` p ) = D )
24		simplr	|- ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> c = C )
25		simpr	|- ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> d = D )
26	24 25	oveq12d	|- ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( c Func d ) = ( C Func D ) )
27		simpllr	|- ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( p = <. C , D >. /\ e = E ) )
28	27	simprd	|- ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> e = E )
29	24 28	oveq12d	|- ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( c Func e ) = ( C Func E ) )
30	25 28	oveq12d	|- ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( d FuncCat e ) = ( D FuncCat E ) )
31	30	fveq2d	|- ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( oppCat ` ( d FuncCat e ) ) = ( oppCat ` ( D FuncCat E ) ) )
32	1	fveq2i	|- ( oppCat ` R ) = ( oppCat ` ( D FuncCat E ) )
33	6 32	eqtri	|- O = ( oppCat ` ( D FuncCat E ) )
34	31 33	eqtr4di	|- ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( oppCat ` ( d FuncCat e ) ) = O )
35	24 28	oveq12d	|- ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( c FuncCat e ) = ( C FuncCat E ) )
36	35	fveq2d	|- ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( oppCat ` ( c FuncCat e ) ) = ( oppCat ` ( C FuncCat E ) ) )
37	2	fveq2i	|- ( oppCat ` S ) = ( oppCat ` ( C FuncCat E ) )
38	7 37	eqtri	|- P = ( oppCat ` ( C FuncCat E ) )
39	36 38	eqtr4di	|- ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( oppCat ` ( c FuncCat e ) ) = P )
40	34 39	oveq12d	|- ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( ( oppCat ` ( d FuncCat e ) ) UP ( oppCat ` ( c FuncCat e ) ) ) = ( O UP P ) )
41	25 28	opeq12d	|- ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> <. d , e >. = <. D , E >. )
42	41	fvoveq1d	|- ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( oppFunc ` ( <. d , e >. -o.F f ) ) = ( oppFunc ` ( <. D , E >. -o.F f ) ) )
43		eqidd	|- ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> x = x )
44	40 42 43	oveq123d	|- ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( ( oppFunc ` ( <. d , e >. -o.F f ) ) ( ( oppCat ` ( d FuncCat e ) ) UP ( oppCat ` ( c FuncCat e ) ) ) x ) = ( ( oppFunc ` ( <. D , E >. -o.F f ) ) ( O UP P ) x ) )
45	26 29 44	mpoeq123dv	|- ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( oppFunc ` ( <. d , e >. -o.F f ) ) ( ( oppCat ` ( d FuncCat e ) ) UP ( oppCat ` ( c FuncCat e ) ) ) x ) ) = ( f e. ( C Func D ) , x e. ( C Func E ) |-> ( ( oppFunc ` ( <. D , E >. -o.F f ) ) ( O UP P ) x ) ) )
46	17 23 45	csbied2	|- ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) -> [_ ( 2nd ` p ) / d ]_ ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( oppFunc ` ( <. d , e >. -o.F f ) ) ( ( oppCat ` ( d FuncCat e ) ) UP ( oppCat ` ( c FuncCat e ) ) ) x ) ) = ( f e. ( C Func D ) , x e. ( C Func E ) |-> ( ( oppFunc ` ( <. D , E >. -o.F f ) ) ( O UP P ) x ) ) )
47	10 16 46	csbied2	|- ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) -> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( oppFunc ` ( <. d , e >. -o.F f ) ) ( ( oppCat ` ( d FuncCat e ) ) UP ( oppCat ` ( c FuncCat e ) ) ) x ) ) = ( f e. ( C Func D ) , x e. ( C Func E ) |-> ( ( oppFunc ` ( <. D , E >. -o.F f ) ) ( O UP P ) x ) ) )
48	3	elexd	|- ( ph -> C e. _V )
49	4	elexd	|- ( ph -> D e. _V )
50	48 49	opelxpd	|- ( ph -> <. C , D >. e. ( _V X. _V ) )
51	5	elexd	|- ( ph -> E e. _V )
52		ovex	|- ( C Func D ) e. _V
53		ovex	|- ( C Func E ) e. _V
54	52 53	mpoex	|- ( f e. ( C Func D ) , x e. ( C Func E ) |-> ( ( oppFunc ` ( <. D , E >. -o.F f ) ) ( O UP P ) x ) ) e. _V
55	54	a1i	|- ( ph -> ( f e. ( C Func D ) , x e. ( C Func E ) |-> ( ( oppFunc ` ( <. D , E >. -o.F f ) ) ( O UP P ) x ) ) e. _V )
56	9 47 50 51 55	ovmpod	|- ( ph -> ( <. C , D >. Ran E ) = ( f e. ( C Func D ) , x e. ( C Func E ) |-> ( ( oppFunc ` ( <. D , E >. -o.F f ) ) ( O UP P ) x ) ) )