Theorem ranval

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

	Ref	Expression
Hypotheses	lanval.r	$$⊢R=D\mathrm{FuncCat}E$$
	lanval.s	$$⊢S=C\mathrm{FuncCat}E$$
	lanval.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
	lanval.x	$$⊢\phi \to X\in \left(C\mathrm{Func}E\right)$$
	ranval.k	No typesetting found for |- ( ph -> ( <. D , E >. -o.F F ) = <. J , K >. ) with typecode |-
	ranval.o	$$⊢O=\mathrm{oppCat}\left(R\right)$$
	ranval.p	$$⊢P=\mathrm{oppCat}\left(S\right)$$
Assertion	ranval	Could not format assertion : No typesetting found for |- ( ph -> ( F ( <. C , D >. Ran E ) X ) = ( <. J , tpos K >. ( O UP P ) X ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		lanval.r	$$⊢R=D\mathrm{FuncCat}E$$
2		lanval.s	$$⊢S=C\mathrm{FuncCat}E$$
3		lanval.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
4		lanval.x	$$⊢\phi \to X\in \left(C\mathrm{Func}E\right)$$
5		ranval.k	Could not format ( ph -> ( <. D , E >. -o.F F ) = <. J , K >. ) : No typesetting found for |- ( ph -> ( <. D , E >. -o.F F ) = <. J , K >. ) with typecode |-
6		ranval.o	$$⊢O=\mathrm{oppCat}\left(R\right)$$
7		ranval.p	$$⊢P=\mathrm{oppCat}\left(S\right)$$
8	3	func1st2nd	$$⊢\phi \to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
9	8	funcrcl2	$$⊢\phi \to C\in \mathrm{Cat}$$
10	8	funcrcl3	$$⊢\phi \to D\in \mathrm{Cat}$$
11	4	func1st2nd	$$⊢\phi \to 1^{st}\left(X\right)\left(C\mathrm{Func}E\right)2^{nd}\left(X\right)$$
12	11	funcrcl3	$$⊢\phi \to E\in \mathrm{Cat}$$
13	1 2 9 10 12 6 7	ranfval	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 |-
14		simprl	$$⊢\left(\phi \wedge \left(f=F\wedge x=X\right)\right)\to f=F$$
15	14	oveq2d	Could not format ( ( ph /\ ( f = F /\ x = X ) ) -> ( <. D , E >. -o.F f ) = ( <. D , E >. -o.F F ) ) : No typesetting found for |- ( ( ph /\ ( f = F /\ x = X ) ) -> ( <. D , E >. -o.F f ) = ( <. D , E >. -o.F F ) ) with typecode |-
16	5	adantr	Could not format ( ( ph /\ ( f = F /\ x = X ) ) -> ( <. D , E >. -o.F F ) = <. J , K >. ) : No typesetting found for |- ( ( ph /\ ( f = F /\ x = X ) ) -> ( <. D , E >. -o.F F ) = <. J , K >. ) with typecode |-
17	15 16	eqtrd	Could not format ( ( ph /\ ( f = F /\ x = X ) ) -> ( <. D , E >. -o.F f ) = <. J , K >. ) : No typesetting found for |- ( ( ph /\ ( f = F /\ x = X ) ) -> ( <. D , E >. -o.F f ) = <. J , K >. ) with typecode |-
18	17	fveq2d	Could not format ( ( ph /\ ( f = F /\ x = X ) ) -> ( oppFunc ` ( <. D , E >. -o.F f ) ) = ( oppFunc ` <. J , K >. ) ) : No typesetting found for |- ( ( ph /\ ( f = F /\ x = X ) ) -> ( oppFunc ` ( <. D , E >. -o.F f ) ) = ( oppFunc ` <. J , K >. ) ) with typecode |-
19		df-ov	Could not format ( J oppFunc K ) = ( oppFunc ` <. J , K >. ) : No typesetting found for |- ( J oppFunc K ) = ( oppFunc ` <. J , K >. ) with typecode |-
20	1 12 2 3 5	prcoffunca2	$$⊢\phi \to J\left(R\mathrm{Func}S\right)K$$
21		oppfval	Could not format ( J ( R Func S ) K -> ( J oppFunc K ) = <. J , tpos K >. ) : No typesetting found for |- ( J ( R Func S ) K -> ( J oppFunc K ) = <. J , tpos K >. ) with typecode |-
22	20 21	syl	Could not format ( ph -> ( J oppFunc K ) = <. J , tpos K >. ) : No typesetting found for |- ( ph -> ( J oppFunc K ) = <. J , tpos K >. ) with typecode |-
23	19 22	eqtr3id	Could not format ( ph -> ( oppFunc ` <. J , K >. ) = <. J , tpos K >. ) : No typesetting found for |- ( ph -> ( oppFunc ` <. J , K >. ) = <. J , tpos K >. ) with typecode |-
24	23	adantr	Could not format ( ( ph /\ ( f = F /\ x = X ) ) -> ( oppFunc ` <. J , K >. ) = <. J , tpos K >. ) : No typesetting found for |- ( ( ph /\ ( f = F /\ x = X ) ) -> ( oppFunc ` <. J , K >. ) = <. J , tpos K >. ) with typecode |-
25	18 24	eqtrd	Could not format ( ( ph /\ ( f = F /\ x = X ) ) -> ( oppFunc ` ( <. D , E >. -o.F f ) ) = <. J , tpos K >. ) : No typesetting found for |- ( ( ph /\ ( f = F /\ x = X ) ) -> ( oppFunc ` ( <. D , E >. -o.F f ) ) = <. J , tpos K >. ) with typecode |-
26		simprr	$$⊢\left(\phi \wedge \left(f=F\wedge x=X\right)\right)\to x=X$$
27	25 26	oveq12d	Could not format ( ( ph /\ ( f = F /\ x = X ) ) -> ( ( oppFunc ` ( <. D , E >. -o.F f ) ) ( O UP P ) x ) = ( <. J , tpos K >. ( O UP P ) X ) ) : No typesetting found for |- ( ( ph /\ ( f = F /\ x = X ) ) -> ( ( oppFunc ` ( <. D , E >. -o.F f ) ) ( O UP P ) x ) = ( <. J , tpos K >. ( O UP P ) X ) ) with typecode |-
28		ovexd	Could not format ( ph -> ( <. J , tpos K >. ( O UP P ) X ) e. _V ) : No typesetting found for |- ( ph -> ( <. J , tpos K >. ( O UP P ) X ) e. _V ) with typecode |-
29	13 27 3 4 28	ovmpod	Could not format ( ph -> ( F ( <. C , D >. Ran E ) X ) = ( <. J , tpos K >. ( O UP P ) X ) ) : No typesetting found for |- ( ph -> ( F ( <. C , D >. Ran E ) X ) = ( <. J , tpos K >. ( O UP P ) X ) ) with typecode |-