Metamath Proof Explorer

Theorem ranup

Description: The universal property of the right Kan extension; expressed explicitly. (Contributed by Zhi Wang, 5-Nov-2025)

Ref Expression
Hypotheses lanup.s 
|- S = ( C FuncCat E )
lanup.m 
|- M = ( D Nat E )
lanup.n 
|- N = ( C Nat E )
lanup.x 
|- .xb = ( comp ` S )
lanup.f 
|- ( ph -> F e. ( C Func D ) )
lanup.l 
|- ( ph -> L e. ( D Func E ) )
ranup.a 
|- ( ph -> A e. ( ( L o.func F ) N X ) )
Assertion ranup 
|- ( ph -> ( L ( F ( <. C , D >. Ran E ) X ) A <-> A. l e. ( D Func E ) A. a e. ( ( l o.func F ) N X ) E! b e. ( l M L ) a = ( A ( <. ( l o.func F ) , ( L o.func F ) >. .xb X ) ( b o. ( 1st ` F ) ) ) ) )

Proof

Step Hyp Ref Expression
1 lanup.s 
 |-  S = ( C FuncCat E )
2 lanup.m 
 |-  M = ( D Nat E )
3 lanup.n 
 |-  N = ( C Nat E )
4 lanup.x 
 |-  .xb = ( comp ` S )
5 lanup.f 
 |-  ( ph -> F e. ( C Func D ) )
6 lanup.l 
 |-  ( ph -> L e. ( D Func E ) )
7 ranup.a 
 |-  ( ph -> A e. ( ( L o.func F ) N X ) )
8 eqid 
 |-  ( D FuncCat E ) = ( D FuncCat E )
9 8 fucbas 
 |-  ( D Func E ) = ( Base ` ( D FuncCat E ) )
10 1 fucbas 
 |-  ( C Func E ) = ( Base ` S )
11 8 2 fuchom 
 |-  M = ( Hom ` ( D FuncCat E ) )
12 1 3 fuchom 
 |-  N = ( Hom ` S )
13 3 natrcl 
 |-  ( A e. ( ( L o.func F ) N X ) -> ( ( L o.func F ) e. ( C Func E ) /\ X e. ( C Func E ) ) )
14 7 13 syl 
 |-  ( ph -> ( ( L o.func F ) e. ( C Func E ) /\ X e. ( C Func E ) ) )
15 14 simprd 
 |-  ( ph -> X e. ( C Func E ) )
16 15 func1st2nd 
 |-  ( ph -> ( 1st ` X ) ( C Func E ) ( 2nd ` X ) )
17 16 funcrcl3 
 |-  ( ph -> E e. Cat )
18 opex 
 |-  <. D , E >. e. _V
19 18 a1i 
 |-  ( ph -> <. D , E >. e. _V )
20 5 19 prcofelvv 
 |-  ( ph -> ( <. D , E >. -o.F F ) e. ( _V X. _V ) )
21 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 ) ) >. )
22 20 21 syl 
 |-  ( ph -> ( <. D , E >. -o.F F ) = <. ( 1st ` ( <. D , E >. -o.F F ) ) , ( 2nd ` ( <. D , E >. -o.F F ) ) >. )
23 8 17 1 5 22 prcoffunca2 
 |-  ( ph -> ( 1st ` ( <. D , E >. -o.F F ) ) ( ( D FuncCat E ) Func S ) ( 2nd ` ( <. D , E >. -o.F F ) ) )
24 eqidd 
 |-  ( ph -> ( 1st ` ( <. D , E >. -o.F F ) ) = ( 1st ` ( <. D , E >. -o.F F ) ) )
25 6 24 prcof1 
 |-  ( ph -> ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) = ( L o.func F ) )
26 25 oveq1d 
 |-  ( ph -> ( ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) N X ) = ( ( L o.func F ) N X ) )
27 7 26 eleqtrrd 
 |-  ( ph -> A e. ( ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) N X ) )
28 eqid 
 |-  ( oppCat ` ( D FuncCat E ) ) = ( oppCat ` ( D FuncCat E ) )
29 eqid 
 |-  ( oppCat ` S ) = ( oppCat ` S )
30 9 10 11 12 4 15 23 6 27 28 29 oppcup 
 |-  ( ph -> ( L ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , tpos ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( ( oppCat ` ( D FuncCat E ) ) UP ( oppCat ` S ) ) X ) A <-> A. l e. ( D Func E ) A. a e. ( ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) N X ) E! b e. ( l M L ) a = ( A ( <. ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb X ) ( ( l ( 2nd ` ( <. D , E >. -o.F F ) ) L ) ` b ) ) ) )
31 1 fveq2i 
 |-  ( oppCat ` S ) = ( oppCat ` ( C FuncCat E ) )
32 28 31 22 5 ranval2 
 |-  ( ph -> ( F ( <. C , D >. Ran E ) X ) = ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , tpos ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( ( oppCat ` ( D FuncCat E ) ) UP ( oppCat ` S ) ) X ) )
33 32 breqd 
 |-  ( ph -> ( L ( F ( <. C , D >. Ran E ) X ) A <-> L ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , tpos ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( ( oppCat ` ( D FuncCat E ) ) UP ( oppCat ` S ) ) X ) A ) )
34 simpr 
 |-  ( ( ph /\ l e. ( D Func E ) ) -> l e. ( D Func E ) )
35 eqidd 
 |-  ( ( ph /\ l e. ( D Func E ) ) -> ( 1st ` ( <. D , E >. -o.F F ) ) = ( 1st ` ( <. D , E >. -o.F F ) ) )
36 34 35 prcof1 
 |-  ( ( ph /\ l e. ( D Func E ) ) -> ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) = ( l o.func F ) )
37 36 eqcomd 
 |-  ( ( ph /\ l e. ( D Func E ) ) -> ( l o.func F ) = ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) )
38 37 oveq1d 
 |-  ( ( ph /\ l e. ( D Func E ) ) -> ( ( l o.func F ) N X ) = ( ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) N X ) )
39 36 ad2antrr 
 |-  ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( ( l o.func F ) N X ) ) /\ b e. ( l M L ) ) -> ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) = ( l o.func F ) )
40 25 ad3antrrr 
 |-  ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( ( l o.func F ) N X ) ) /\ b e. ( l M L ) ) -> ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) = ( L o.func F ) )
41 39 40 opeq12d 
 |-  ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( ( l o.func F ) N X ) ) /\ b e. ( l M L ) ) -> <. ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. = <. ( l o.func F ) , ( L o.func F ) >. )
42 41 oveq1d 
 |-  ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( ( l o.func F ) N X ) ) /\ b e. ( l M L ) ) -> ( <. ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb X ) = ( <. ( l o.func F ) , ( L o.func F ) >. .xb X ) )
43 eqidd 
 |-  ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( ( l o.func F ) N X ) ) /\ b e. ( l M L ) ) -> A = A )
44 simpr 
 |-  ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( ( l o.func F ) N X ) ) /\ b e. ( l M L ) ) -> b e. ( l M L ) )
45 eqidd 
 |-  ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( ( l o.func F ) N X ) ) /\ b e. ( l M L ) ) -> ( 2nd ` ( <. D , E >. -o.F F ) ) = ( 2nd ` ( <. D , E >. -o.F F ) ) )
46 5 ad3antrrr 
 |-  ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( ( l o.func F ) N X ) ) /\ b e. ( l M L ) ) -> F e. ( C Func D ) )
47 2 44 45 46 prcof21a 
 |-  ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( ( l o.func F ) N X ) ) /\ b e. ( l M L ) ) -> ( ( l ( 2nd ` ( <. D , E >. -o.F F ) ) L ) ` b ) = ( b o. ( 1st ` F ) ) )
48 42 43 47 oveq123d 
 |-  ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( ( l o.func F ) N X ) ) /\ b e. ( l M L ) ) -> ( A ( <. ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb X ) ( ( l ( 2nd ` ( <. D , E >. -o.F F ) ) L ) ` b ) ) = ( A ( <. ( l o.func F ) , ( L o.func F ) >. .xb X ) ( b o. ( 1st ` F ) ) ) )
49 48 eqcomd 
 |-  ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( ( l o.func F ) N X ) ) /\ b e. ( l M L ) ) -> ( A ( <. ( l o.func F ) , ( L o.func F ) >. .xb X ) ( b o. ( 1st ` F ) ) ) = ( A ( <. ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb X ) ( ( l ( 2nd ` ( <. D , E >. -o.F F ) ) L ) ` b ) ) )
50 49 eqeq2d 
 |-  ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( ( l o.func F ) N X ) ) /\ b e. ( l M L ) ) -> ( a = ( A ( <. ( l o.func F ) , ( L o.func F ) >. .xb X ) ( b o. ( 1st ` F ) ) ) <-> a = ( A ( <. ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb X ) ( ( l ( 2nd ` ( <. D , E >. -o.F F ) ) L ) ` b ) ) ) )
51 50 reubidva 
 |-  ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( ( l o.func F ) N X ) ) -> ( E! b e. ( l M L ) a = ( A ( <. ( l o.func F ) , ( L o.func F ) >. .xb X ) ( b o. ( 1st ` F ) ) ) <-> E! b e. ( l M L ) a = ( A ( <. ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb X ) ( ( l ( 2nd ` ( <. D , E >. -o.F F ) ) L ) ` b ) ) ) )
52 38 51 raleqbidva 
 |-  ( ( ph /\ l e. ( D Func E ) ) -> ( A. a e. ( ( l o.func F ) N X ) E! b e. ( l M L ) a = ( A ( <. ( l o.func F ) , ( L o.func F ) >. .xb X ) ( b o. ( 1st ` F ) ) ) <-> A. a e. ( ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) N X ) E! b e. ( l M L ) a = ( A ( <. ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb X ) ( ( l ( 2nd ` ( <. D , E >. -o.F F ) ) L ) ` b ) ) ) )
53 52 ralbidva 
 |-  ( ph -> ( A. l e. ( D Func E ) A. a e. ( ( l o.func F ) N X ) E! b e. ( l M L ) a = ( A ( <. ( l o.func F ) , ( L o.func F ) >. .xb X ) ( b o. ( 1st ` F ) ) ) <-> A. l e. ( D Func E ) A. a e. ( ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) N X ) E! b e. ( l M L ) a = ( A ( <. ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb X ) ( ( l ( 2nd ` ( <. D , E >. -o.F F ) ) L ) ` b ) ) ) )
54 30 33 53 3bitr4d 
 |-  ( ph -> ( L ( F ( <. C , D >. Ran E ) X ) A <-> A. l e. ( D Func E ) A. a e. ( ( l o.func F ) N X ) E! b e. ( l M L ) a = ( A ( <. ( l o.func F ) , ( L o.func F ) >. .xb X ) ( b o. ( 1st ` F ) ) ) ) )