Metamath Proof Explorer

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 FuncCat E )
lanval.s 
|- S = ( C FuncCat E )
lanval.f 
|- ( ph -> F e. ( C Func D ) )
lanval.x 
|- ( ph -> X e. ( C Func E ) )
ranval.k 
|- ( ph -> ( <. D , E >. -o.F F ) = <. J , K >. )
ranval.o 
|- O = ( oppCat ` R )
ranval.p 
|- P = ( oppCat ` S )
Assertion ranval 
|- ( ph -> ( F ( <. C , D >. Ran E ) X ) = ( <. J , tpos K >. ( O UP P ) X ) )

Proof

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