Metamath Proof Explorer

Theorem lanfval

Description: Value of the function generating the set of left Kan extensions. (Contributed by Zhi Wang, 3-Nov-2025)

Ref Expression
Hypotheses lanfval.r 
|- R = ( D FuncCat E )
lanfval.s 
|- S = ( C FuncCat E )
lanfval.c 
|- ( ph -> C e. U )
lanfval.d 
|- ( ph -> D e. V )
lanfval.e 
|- ( ph -> E e. W )
Assertion lanfval 
|- ( ph -> ( <. C , D >. Lan E ) = ( f e. ( C Func D ) , x e. ( C Func E ) |-> ( ( <. D , E >. -o.F f ) ( R UP S ) x ) ) )

Proof

Step Hyp Ref Expression
1 lanfval.r 
 |-  R = ( D FuncCat E )
2 lanfval.s 
 |-  S = ( C FuncCat E )
3 lanfval.c 
 |-  ( ph -> C e. U )
4 lanfval.d 
 |-  ( ph -> D e. V )
5 lanfval.e 
 |-  ( ph -> E e. W )
6 df-lan 
 |-  Lan = ( p e. ( _V X. _V ) , e e. _V |-> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( <. d , e >. -o.F f ) ( ( d FuncCat e ) UP ( c FuncCat e ) ) x ) ) )
7 6 a1i 
 |-  ( ph -> Lan = ( p e. ( _V X. _V ) , e e. _V |-> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( <. d , e >. -o.F f ) ( ( d FuncCat e ) UP ( c FuncCat e ) ) x ) ) ) )
8 fvexd 
 |-  ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) -> ( 1st ` p ) e. _V )
9 simprl 
 |-  ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) -> p = <. C , D >. )
10 9 fveq2d 
 |-  ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) -> ( 1st ` p ) = ( 1st ` <. C , D >. ) )
11 op1stg 
 |-  ( ( C e. U /\ D e. V ) -> ( 1st ` <. C , D >. ) = C )
12 3 4 11 syl2anc 
 |-  ( ph -> ( 1st ` <. C , D >. ) = C )
13 12 adantr 
 |-  ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) -> ( 1st ` <. C , D >. ) = C )
14 10 13 eqtrd 
 |-  ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) -> ( 1st ` p ) = C )
15 fvexd 
 |-  ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) -> ( 2nd ` p ) e. _V )
16 simplrl 
 |-  ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) -> p = <. C , D >. )
17 16 fveq2d 
 |-  ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) -> ( 2nd ` p ) = ( 2nd ` <. C , D >. ) )
18 op2ndg 
 |-  ( ( C e. U /\ D e. V ) -> ( 2nd ` <. C , D >. ) = D )
19 3 4 18 syl2anc 
 |-  ( ph -> ( 2nd ` <. C , D >. ) = D )
20 19 ad2antrr 
 |-  ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) -> ( 2nd ` <. C , D >. ) = D )
21 17 20 eqtrd 
 |-  ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) -> ( 2nd ` p ) = D )
22 simplr 
 |-  ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> c = C )
23 simpr 
 |-  ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> d = D )
24 22 23 oveq12d 
 |-  ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( c Func d ) = ( C Func D ) )
25 simpllr 
 |-  ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( p = <. C , D >. /\ e = E ) )
26 25 simprd 
 |-  ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> e = E )
27 22 26 oveq12d 
 |-  ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( c Func e ) = ( C Func E ) )
28 23 26 oveq12d 
 |-  ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( d FuncCat e ) = ( D FuncCat E ) )
29 28 1 eqtr4di 
 |-  ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( d FuncCat e ) = R )
30 22 26 oveq12d 
 |-  ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( c FuncCat e ) = ( C FuncCat E ) )
31 30 2 eqtr4di 
 |-  ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( c FuncCat e ) = S )
32 29 31 oveq12d 
 |-  ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( ( d FuncCat e ) UP ( c FuncCat e ) ) = ( R UP S ) )
33 23 26 opeq12d 
 |-  ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> <. d , e >. = <. D , E >. )
34 33 oveq1d 
 |-  ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( <. d , e >. -o.F f ) = ( <. D , E >. -o.F f ) )
35 eqidd 
 |-  ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> x = x )
36 32 34 35 oveq123d 
 |-  ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( ( <. d , e >. -o.F f ) ( ( d FuncCat e ) UP ( c FuncCat e ) ) x ) = ( ( <. D , E >. -o.F f ) ( R UP S ) x ) )
37 24 27 36 mpoeq123dv 
 |-  ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( <. d , e >. -o.F f ) ( ( d FuncCat e ) UP ( c FuncCat e ) ) x ) ) = ( f e. ( C Func D ) , x e. ( C Func E ) |-> ( ( <. D , E >. -o.F f ) ( R UP S ) x ) ) )
38 15 21 37 csbied2 
 |-  ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) -> [_ ( 2nd ` p ) / d ]_ ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( <. d , e >. -o.F f ) ( ( d FuncCat e ) UP ( c FuncCat e ) ) x ) ) = ( f e. ( C Func D ) , x e. ( C Func E ) |-> ( ( <. D , E >. -o.F f ) ( R UP S ) x ) ) )
39 8 14 38 csbied2 
 |-  ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) -> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( <. d , e >. -o.F f ) ( ( d FuncCat e ) UP ( c FuncCat e ) ) x ) ) = ( f e. ( C Func D ) , x e. ( C Func E ) |-> ( ( <. D , E >. -o.F f ) ( R UP S ) x ) ) )
40 3 elexd 
 |-  ( ph -> C e. _V )
41 4 elexd 
 |-  ( ph -> D e. _V )
42 40 41 opelxpd 
 |-  ( ph -> <. C , D >. e. ( _V X. _V ) )
43 5 elexd 
 |-  ( ph -> E e. _V )
44 ovex 
 |-  ( C Func D ) e. _V
45 ovex 
 |-  ( C Func E ) e. _V
46 44 45 mpoex 
 |-  ( f e. ( C Func D ) , x e. ( C Func E ) |-> ( ( <. D , E >. -o.F f ) ( R UP S ) x ) ) e. _V
47 46 a1i 
 |-  ( ph -> ( f e. ( C Func D ) , x e. ( C Func E ) |-> ( ( <. D , E >. -o.F f ) ( R UP S ) x ) ) e. _V )
48 7 39 42 43 47 ovmpod 
 |-  ( ph -> ( <. C , D >. Lan E ) = ( f e. ( C Func D ) , x e. ( C Func E ) |-> ( ( <. D , E >. -o.F f ) ( R UP S ) x ) ) )