Metamath Proof Explorer

Theorem lanup

Description: The universal property of the left Kan extension; expressed explicitly. (Contributed by Zhi Wang, 4-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 ) )
lanup.a 
|- ( ph -> A e. ( X N ( L o.func F ) ) )
Assertion lanup 
|- ( ph -> ( L ( F ( <. C , D >. Lan E ) X ) A <-> A. l e. ( D Func E ) A. a e. ( X N ( l o.func F ) ) E! b e. ( L M l ) a = ( ( b o. ( 1st ` F ) ) ( <. X , ( L o.func F ) >. .xb ( l o.func F ) ) A ) ) )

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 lanup.a 
 |-  ( ph -> A e. ( X N ( L o.func F ) ) )
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. ( X N ( L o.func F ) ) -> ( X e. ( C Func E ) /\ ( L o.func F ) e. ( C Func E ) ) )
14 7 13 syl 
 |-  ( ph -> ( X e. ( C Func E ) /\ ( L o.func F ) e. ( C Func E ) ) )
15 14 simpld 
 |-  ( 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 8 17 1 5 prcoffunca 
 |-  ( ph -> ( <. D , E >. -o.F F ) e. ( ( D FuncCat E ) Func S ) )
19 18 func1st2nd 
 |-  ( ph -> ( 1st ` ( <. D , E >. -o.F F ) ) ( ( D FuncCat E ) Func S ) ( 2nd ` ( <. D , E >. -o.F F ) ) )
20 eqidd 
 |-  ( ph -> ( 1st ` ( <. D , E >. -o.F F ) ) = ( 1st ` ( <. D , E >. -o.F F ) ) )
21 6 20 prcof1 
 |-  ( ph -> ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) = ( L o.func F ) )
22 21 oveq2d 
 |-  ( ph -> ( X N ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) ) = ( X N ( L o.func F ) ) )
23 7 22 eleqtrrd 
 |-  ( ph -> A e. ( X N ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) ) )
24 9 10 11 12 4 15 19 6 23 isup 
 |-  ( ph -> ( L ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( ( D FuncCat E ) UP S ) X ) A <-> A. l e. ( D Func E ) A. a e. ( X N ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) E! b e. ( L M l ) a = ( ( ( L ( 2nd ` ( <. D , E >. -o.F F ) ) l ) ` b ) ( <. X , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) A ) ) )
25 eqidd 
 |-  ( ph -> ( <. D , E >. -o.F F ) = ( <. D , E >. -o.F F ) )
26 8 1 5 15 25 lanval 
 |-  ( ph -> ( F ( <. C , D >. Lan E ) X ) = ( ( <. D , E >. -o.F F ) ( ( D FuncCat E ) UP S ) X ) )
27 26 breqd 
 |-  ( ph -> ( L ( F ( <. C , D >. Lan E ) X ) A <-> L ( ( <. D , E >. -o.F F ) ( ( D FuncCat E ) UP S ) X ) A ) )
28 18 up1st2ndb 
 |-  ( ph -> ( L ( ( <. D , E >. -o.F F ) ( ( D FuncCat E ) UP S ) X ) A <-> L ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( ( D FuncCat E ) UP S ) X ) A ) )
29 27 28 bitrd 
 |-  ( ph -> ( L ( F ( <. C , D >. Lan E ) X ) A <-> L ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( ( D FuncCat E ) UP S ) X ) A ) )
30 simpr 
 |-  ( ( ph /\ l e. ( D Func E ) ) -> l e. ( D Func E ) )
31 eqidd 
 |-  ( ( ph /\ l e. ( D Func E ) ) -> ( 1st ` ( <. D , E >. -o.F F ) ) = ( 1st ` ( <. D , E >. -o.F F ) ) )
32 30 31 prcof1 
 |-  ( ( ph /\ l e. ( D Func E ) ) -> ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) = ( l o.func F ) )
33 32 eqcomd 
 |-  ( ( ph /\ l e. ( D Func E ) ) -> ( l o.func F ) = ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) )
34 33 oveq2d 
 |-  ( ( ph /\ l e. ( D Func E ) ) -> ( X N ( l o.func F ) ) = ( X N ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) )
35 21 ad3antrrr 
 |-  ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( X N ( l o.func F ) ) ) /\ b e. ( L M l ) ) -> ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) = ( L o.func F ) )
36 35 opeq2d 
 |-  ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( X N ( l o.func F ) ) ) /\ b e. ( L M l ) ) -> <. X , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. = <. X , ( L o.func F ) >. )
37 32 ad2antrr 
 |-  ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( X N ( l o.func F ) ) ) /\ b e. ( L M l ) ) -> ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) = ( l o.func F ) )
38 36 37 oveq12d 
 |-  ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( X N ( l o.func F ) ) ) /\ b e. ( L M l ) ) -> ( <. X , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) = ( <. X , ( L o.func F ) >. .xb ( l o.func F ) ) )
39 simpr 
 |-  ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( X N ( l o.func F ) ) ) /\ b e. ( L M l ) ) -> b e. ( L M l ) )
40 eqidd 
 |-  ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( X N ( l o.func F ) ) ) /\ b e. ( L M l ) ) -> ( 2nd ` ( <. D , E >. -o.F F ) ) = ( 2nd ` ( <. D , E >. -o.F F ) ) )
41 5 ad3antrrr 
 |-  ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( X N ( l o.func F ) ) ) /\ b e. ( L M l ) ) -> F e. ( C Func D ) )
42 2 39 40 41 prcof21a 
 |-  ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( X N ( l o.func F ) ) ) /\ b e. ( L M l ) ) -> ( ( L ( 2nd ` ( <. D , E >. -o.F F ) ) l ) ` b ) = ( b o. ( 1st ` F ) ) )
43 eqidd 
 |-  ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( X N ( l o.func F ) ) ) /\ b e. ( L M l ) ) -> A = A )
44 38 42 43 oveq123d 
 |-  ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( X N ( l o.func F ) ) ) /\ b e. ( L M l ) ) -> ( ( ( L ( 2nd ` ( <. D , E >. -o.F F ) ) l ) ` b ) ( <. X , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) A ) = ( ( b o. ( 1st ` F ) ) ( <. X , ( L o.func F ) >. .xb ( l o.func F ) ) A ) )
45 44 eqcomd 
 |-  ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( X N ( l o.func F ) ) ) /\ b e. ( L M l ) ) -> ( ( b o. ( 1st ` F ) ) ( <. X , ( L o.func F ) >. .xb ( l o.func F ) ) A ) = ( ( ( L ( 2nd ` ( <. D , E >. -o.F F ) ) l ) ` b ) ( <. X , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) A ) )
46 45 eqeq2d 
 |-  ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( X N ( l o.func F ) ) ) /\ b e. ( L M l ) ) -> ( a = ( ( b o. ( 1st ` F ) ) ( <. X , ( L o.func F ) >. .xb ( l o.func F ) ) A ) <-> a = ( ( ( L ( 2nd ` ( <. D , E >. -o.F F ) ) l ) ` b ) ( <. X , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) A ) ) )
47 46 reubidva 
 |-  ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( X N ( l o.func F ) ) ) -> ( E! b e. ( L M l ) a = ( ( b o. ( 1st ` F ) ) ( <. X , ( L o.func F ) >. .xb ( l o.func F ) ) A ) <-> E! b e. ( L M l ) a = ( ( ( L ( 2nd ` ( <. D , E >. -o.F F ) ) l ) ` b ) ( <. X , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) A ) ) )
48 34 47 raleqbidva 
 |-  ( ( ph /\ l e. ( D Func E ) ) -> ( A. a e. ( X N ( l o.func F ) ) E! b e. ( L M l ) a = ( ( b o. ( 1st ` F ) ) ( <. X , ( L o.func F ) >. .xb ( l o.func F ) ) A ) <-> A. a e. ( X N ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) E! b e. ( L M l ) a = ( ( ( L ( 2nd ` ( <. D , E >. -o.F F ) ) l ) ` b ) ( <. X , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) A ) ) )
49 48 ralbidva 
 |-  ( ph -> ( A. l e. ( D Func E ) A. a e. ( X N ( l o.func F ) ) E! b e. ( L M l ) a = ( ( b o. ( 1st ` F ) ) ( <. X , ( L o.func F ) >. .xb ( l o.func F ) ) A ) <-> A. l e. ( D Func E ) A. a e. ( X N ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) E! b e. ( L M l ) a = ( ( ( L ( 2nd ` ( <. D , E >. -o.F F ) ) l ) ` b ) ( <. X , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) A ) ) )
50 24 29 49 3bitr4d 
 |-  ( ph -> ( L ( F ( <. C , D >. Lan E ) X ) A <-> A. l e. ( D Func E ) A. a e. ( X N ( l o.func F ) ) E! b e. ( L M l ) a = ( ( b o. ( 1st ` F ) ) ( <. X , ( L o.func F ) >. .xb ( l o.func F ) ) A ) ) )