Metamath Proof Explorer

Theorem prcofvalg

Description: Value of the pre-composition functor. (Contributed by Zhi Wang, 2-Nov-2025)

Ref Expression
Hypotheses prcofvalg.b 
|- B = ( D Func E )
prcofvalg.n 
|- N = ( D Nat E )
prcofvalg.f 
|- ( ph -> F e. U )
prcofvalg.p 
|- ( ph -> P e. V )
prcofvalg.d 
|- ( ph -> ( 1st ` P ) = D )
prcofvalg.e 
|- ( ph -> ( 2nd ` P ) = E )
Assertion prcofvalg 
|- ( ph -> ( P -o.F F ) = <. ( k e. B |-> ( k o.func F ) ) , ( k e. B , l e. B |-> ( a e. ( k N l ) |-> ( a o. ( 1st ` F ) ) ) ) >. )

Proof

Step Hyp Ref Expression
1 prcofvalg.b 
 |-  B = ( D Func E )
2 prcofvalg.n 
 |-  N = ( D Nat E )
3 prcofvalg.f 
 |-  ( ph -> F e. U )
4 prcofvalg.p 
 |-  ( ph -> P e. V )
5 prcofvalg.d 
 |-  ( ph -> ( 1st ` P ) = D )
6 prcofvalg.e 
 |-  ( ph -> ( 2nd ` P ) = E )
7 df-prcof 
 |-  -o.F = ( p e. _V , f e. _V |-> [_ ( 1st ` p ) / d ]_ [_ ( 2nd ` p ) / e ]_ [_ ( d Func e ) / b ]_ <. ( k e. b |-> ( k o.func f ) ) , ( k e. b , l e. b |-> ( a e. ( k ( d Nat e ) l ) |-> ( a o. ( 1st ` f ) ) ) ) >. )
8 7 a1i 
 |-  ( ph -> -o.F = ( p e. _V , f e. _V |-> [_ ( 1st ` p ) / d ]_ [_ ( 2nd ` p ) / e ]_ [_ ( d Func e ) / b ]_ <. ( k e. b |-> ( k o.func f ) ) , ( k e. b , l e. b |-> ( a e. ( k ( d Nat e ) l ) |-> ( a o. ( 1st ` f ) ) ) ) >. ) )
9 fvexd 
 |-  ( ( ph /\ ( p = P /\ f = F ) ) -> ( 1st ` p ) e. _V )
10 simprl 
 |-  ( ( ph /\ ( p = P /\ f = F ) ) -> p = P )
11 10 fveq2d 
 |-  ( ( ph /\ ( p = P /\ f = F ) ) -> ( 1st ` p ) = ( 1st ` P ) )
12 5 adantr 
 |-  ( ( ph /\ ( p = P /\ f = F ) ) -> ( 1st ` P ) = D )
13 11 12 eqtrd 
 |-  ( ( ph /\ ( p = P /\ f = F ) ) -> ( 1st ` p ) = D )
14 fvexd 
 |-  ( ( ( ph /\ ( p = P /\ f = F ) ) /\ d = D ) -> ( 2nd ` p ) e. _V )
15 10 adantr 
 |-  ( ( ( ph /\ ( p = P /\ f = F ) ) /\ d = D ) -> p = P )
16 15 fveq2d 
 |-  ( ( ( ph /\ ( p = P /\ f = F ) ) /\ d = D ) -> ( 2nd ` p ) = ( 2nd ` P ) )
17 6 ad2antrr 
 |-  ( ( ( ph /\ ( p = P /\ f = F ) ) /\ d = D ) -> ( 2nd ` P ) = E )
18 16 17 eqtrd 
 |-  ( ( ( ph /\ ( p = P /\ f = F ) ) /\ d = D ) -> ( 2nd ` p ) = E )
19 ovexd 
 |-  ( ( ( ( ph /\ ( p = P /\ f = F ) ) /\ d = D ) /\ e = E ) -> ( d Func e ) e. _V )
20 simplr 
 |-  ( ( ( ( ph /\ ( p = P /\ f = F ) ) /\ d = D ) /\ e = E ) -> d = D )
21 simpr 
 |-  ( ( ( ( ph /\ ( p = P /\ f = F ) ) /\ d = D ) /\ e = E ) -> e = E )
22 20 21 oveq12d 
 |-  ( ( ( ( ph /\ ( p = P /\ f = F ) ) /\ d = D ) /\ e = E ) -> ( d Func e ) = ( D Func E ) )
23 22 1 eqtr4di 
 |-  ( ( ( ( ph /\ ( p = P /\ f = F ) ) /\ d = D ) /\ e = E ) -> ( d Func e ) = B )
24 simpr 
 |-  ( ( ( ( ( ph /\ ( p = P /\ f = F ) ) /\ d = D ) /\ e = E ) /\ b = B ) -> b = B )
25 simp-4r 
 |-  ( ( ( ( ( ph /\ ( p = P /\ f = F ) ) /\ d = D ) /\ e = E ) /\ b = B ) -> ( p = P /\ f = F ) )
26 25 simprd 
 |-  ( ( ( ( ( ph /\ ( p = P /\ f = F ) ) /\ d = D ) /\ e = E ) /\ b = B ) -> f = F )
27 26 oveq2d 
 |-  ( ( ( ( ( ph /\ ( p = P /\ f = F ) ) /\ d = D ) /\ e = E ) /\ b = B ) -> ( k o.func f ) = ( k o.func F ) )
28 24 27 mpteq12dv 
 |-  ( ( ( ( ( ph /\ ( p = P /\ f = F ) ) /\ d = D ) /\ e = E ) /\ b = B ) -> ( k e. b |-> ( k o.func f ) ) = ( k e. B |-> ( k o.func F ) ) )
29 20 21 oveq12d 
 |-  ( ( ( ( ph /\ ( p = P /\ f = F ) ) /\ d = D ) /\ e = E ) -> ( d Nat e ) = ( D Nat E ) )
30 29 2 eqtr4di 
 |-  ( ( ( ( ph /\ ( p = P /\ f = F ) ) /\ d = D ) /\ e = E ) -> ( d Nat e ) = N )
31 30 oveqdr 
 |-  ( ( ( ( ( ph /\ ( p = P /\ f = F ) ) /\ d = D ) /\ e = E ) /\ b = B ) -> ( k ( d Nat e ) l ) = ( k N l ) )
32 26 fveq2d 
 |-  ( ( ( ( ( ph /\ ( p = P /\ f = F ) ) /\ d = D ) /\ e = E ) /\ b = B ) -> ( 1st ` f ) = ( 1st ` F ) )
33 32 coeq2d 
 |-  ( ( ( ( ( ph /\ ( p = P /\ f = F ) ) /\ d = D ) /\ e = E ) /\ b = B ) -> ( a o. ( 1st ` f ) ) = ( a o. ( 1st ` F ) ) )
34 31 33 mpteq12dv 
 |-  ( ( ( ( ( ph /\ ( p = P /\ f = F ) ) /\ d = D ) /\ e = E ) /\ b = B ) -> ( a e. ( k ( d Nat e ) l ) |-> ( a o. ( 1st ` f ) ) ) = ( a e. ( k N l ) |-> ( a o. ( 1st ` F ) ) ) )
35 24 24 34 mpoeq123dv 
 |-  ( ( ( ( ( ph /\ ( p = P /\ f = F ) ) /\ d = D ) /\ e = E ) /\ b = B ) -> ( k e. b , l e. b |-> ( a e. ( k ( d Nat e ) l ) |-> ( a o. ( 1st ` f ) ) ) ) = ( k e. B , l e. B |-> ( a e. ( k N l ) |-> ( a o. ( 1st ` F ) ) ) ) )
36 28 35 opeq12d 
 |-  ( ( ( ( ( ph /\ ( p = P /\ f = F ) ) /\ d = D ) /\ e = E ) /\ b = B ) -> <. ( k e. b |-> ( k o.func f ) ) , ( k e. b , l e. b |-> ( a e. ( k ( d Nat e ) l ) |-> ( a o. ( 1st ` f ) ) ) ) >. = <. ( k e. B |-> ( k o.func F ) ) , ( k e. B , l e. B |-> ( a e. ( k N l ) |-> ( a o. ( 1st ` F ) ) ) ) >. )
37 19 23 36 csbied2 
 |-  ( ( ( ( ph /\ ( p = P /\ f = F ) ) /\ d = D ) /\ e = E ) -> [_ ( d Func e ) / b ]_ <. ( k e. b |-> ( k o.func f ) ) , ( k e. b , l e. b |-> ( a e. ( k ( d Nat e ) l ) |-> ( a o. ( 1st ` f ) ) ) ) >. = <. ( k e. B |-> ( k o.func F ) ) , ( k e. B , l e. B |-> ( a e. ( k N l ) |-> ( a o. ( 1st ` F ) ) ) ) >. )
38 14 18 37 csbied2 
 |-  ( ( ( ph /\ ( p = P /\ f = F ) ) /\ d = D ) -> [_ ( 2nd ` p ) / e ]_ [_ ( d Func e ) / b ]_ <. ( k e. b |-> ( k o.func f ) ) , ( k e. b , l e. b |-> ( a e. ( k ( d Nat e ) l ) |-> ( a o. ( 1st ` f ) ) ) ) >. = <. ( k e. B |-> ( k o.func F ) ) , ( k e. B , l e. B |-> ( a e. ( k N l ) |-> ( a o. ( 1st ` F ) ) ) ) >. )
39 9 13 38 csbied2 
 |-  ( ( ph /\ ( p = P /\ f = F ) ) -> [_ ( 1st ` p ) / d ]_ [_ ( 2nd ` p ) / e ]_ [_ ( d Func e ) / b ]_ <. ( k e. b |-> ( k o.func f ) ) , ( k e. b , l e. b |-> ( a e. ( k ( d Nat e ) l ) |-> ( a o. ( 1st ` f ) ) ) ) >. = <. ( k e. B |-> ( k o.func F ) ) , ( k e. B , l e. B |-> ( a e. ( k N l ) |-> ( a o. ( 1st ` F ) ) ) ) >. )
40 4 elexd 
 |-  ( ph -> P e. _V )
41 3 elexd 
 |-  ( ph -> F e. _V )
42 opex 
 |-  <. ( k e. B |-> ( k o.func F ) ) , ( k e. B , l e. B |-> ( a e. ( k N l ) |-> ( a o. ( 1st ` F ) ) ) ) >. e. _V
43 42 a1i 
 |-  ( ph -> <. ( k e. B |-> ( k o.func F ) ) , ( k e. B , l e. B |-> ( a e. ( k N l ) |-> ( a o. ( 1st ` F ) ) ) ) >. e. _V )
44 8 39 40 41 43 ovmpod 
 |-  ( ph -> ( P -o.F F ) = <. ( k e. B |-> ( k o.func F ) ) , ( k e. B , l e. B |-> ( a e. ( k N l ) |-> ( a o. ( 1st ` F ) ) ) ) >. )