Metamath Proof Explorer

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 = ( oppCat ` ( D FuncCat E ) )
ranval3.p 
|- P = ( oppCat ` ( C FuncCat E ) )
ranval3.k 
|- K = ( <. D , E >. -o.F F )
Assertion ranval3 
|- ( F e. ( C Func D ) -> ( F ( <. C , D >. Ran E ) X ) = ( ( oppFunc ` K ) ( O UP P ) X ) )

Proof

Step Hyp Ref Expression
1 ranval3.o 
 |-  O = ( oppCat ` ( D FuncCat E ) )
2 ranval3.p 
 |-  P = ( oppCat ` ( C FuncCat E ) )
3 ranval3.k 
 |-  K = ( <. D , E >. -o.F F )
4 id 
 |-  ( F e. ( C Func D ) -> F e. ( C Func D ) )
5 opex 
 |-  <. D , E >. e. _V
6 5 a1i 
 |-  ( F e. ( C Func D ) -> <. D , E >. e. _V )
7 4 6 prcofelvv 
 |-  ( F e. ( C Func D ) -> ( <. D , E >. -o.F F ) e. ( _V X. _V ) )
8 1st2nd2 
 |-  ( ( <. 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 ) ) >. )
9 7 8 syl 
 |-  ( F e. ( C Func D ) -> ( <. D , E >. -o.F F ) = <. ( 1st ` ( <. D , E >. -o.F F ) ) , ( 2nd ` ( <. D , E >. -o.F F ) ) >. )
10 1 2 9 4 ranval2 
 |-  ( 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 ) )
11 eqid 
 |-  ( C FuncCat E ) = ( C FuncCat E )
12 11 fucbas 
 |-  ( C Func E ) = ( Base ` ( C FuncCat E ) )
13 2 12 oppcbas 
 |-  ( C Func E ) = ( Base ` P )
14 13 uprcl 
 |-  ( x e. ( ( oppFunc ` K ) ( O UP P ) X ) -> ( ( oppFunc ` K ) e. ( O Func P ) /\ X e. ( C Func E ) ) )
15 14 simprd 
 |-  ( x e. ( ( oppFunc ` K ) ( O UP P ) X ) -> X e. ( C Func E ) )
16 15 adantl 
 |-  ( ( F e. ( C Func D ) /\ x e. ( ( oppFunc ` K ) ( O UP P ) X ) ) -> X e. ( C Func E ) )
17 13 uprcl 
 |-  ( 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 ) ) )
18 17 simprd 
 |-  ( x e. ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , tpos ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( O UP P ) X ) -> X e. ( C Func E ) )
19 18 adantl 
 |-  ( ( 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 ) )
20 eqid 
 |-  ( D FuncCat E ) = ( D FuncCat E )
21 funcrcl 
 |-  ( X e. ( C Func E ) -> ( C e. Cat /\ E e. Cat ) )
22 21 simprd 
 |-  ( X e. ( C Func E ) -> E e. Cat )
23 22 adantl 
 |-  ( ( F e. ( C Func D ) /\ X e. ( C Func E ) ) -> E e. Cat )
24 simpl 
 |-  ( ( F e. ( C Func D ) /\ X e. ( C Func E ) ) -> F e. ( C Func D ) )
25 20 23 11 24 prcoffunca 
 |-  ( ( F e. ( C Func D ) /\ X e. ( C Func E ) ) -> ( <. D , E >. -o.F F ) e. ( ( D FuncCat E ) Func ( C FuncCat E ) ) )
26 3 fveq2i 
 |-  ( oppFunc ` K ) = ( oppFunc ` ( <. D , E >. -o.F F ) )
27 oppfval2 
 |-  ( ( <. 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 ) ) >. )
28 26 27 eqtrid 
 |-  ( ( <. 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 ) ) >. )
29 25 28 syl 
 |-  ( ( 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 ) ) >. )
30 29 oveq1d 
 |-  ( ( 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 ) )
31 30 eleq2d 
 |-  ( ( 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 ) ) )
32 16 19 31 bibiad 
 |-  ( 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 ) ) )
33 32 eqrdv 
 |-  ( 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 ) )
34 10 33 eqtr4d 
 |-  ( F e. ( C Func D ) -> ( F ( <. C , D >. Ran E ) X ) = ( ( oppFunc ` K ) ( O UP P ) X ) )