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\mathrm{FuncCat}E$$
	lanfval.s	$$⊢S=C\mathrm{FuncCat}E$$
	lanfval.c	$$⊢\phi \to C\in U$$
	lanfval.d	$$⊢\phi \to D\in V$$
	lanfval.e	$$⊢\phi \to E\in W$$
	ranfval.o	$$⊢O=\mathrm{oppCat}\left(R\right)$$
	ranfval.p	$$⊢P=\mathrm{oppCat}\left(S\right)$$
Assertion	ranfval	Could not format assertion : No typesetting found for |- ( 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 ) ) ) with typecode |-

Proof

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