Metamath Proof Explorer

Theorem prcofval

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 )
prcofvala.d 
|- ( ph -> D e. V )
prcofvala.e 
|- ( ph -> E e. W )
prcofval.r 
|- Rel R
prcofval.f 
|- ( ph -> F R G )
Assertion prcofval 
|- ( ph -> ( <. D , E >. -o.F <. F , G >. ) = <. ( k e. B |-> ( k o.func <. F , G >. ) ) , ( k e. B , l e. B |-> ( a e. ( k N l ) |-> ( a o. F ) ) ) >. )

Proof

Step Hyp Ref Expression
1 prcofvalg.b 
 |-  B = ( D Func E )
2 prcofvalg.n 
 |-  N = ( D Nat E )
3 prcofvala.d 
 |-  ( ph -> D e. V )
4 prcofvala.e 
 |-  ( ph -> E e. W )
5 prcofval.r 
 |-  Rel R
6 prcofval.f 
 |-  ( ph -> F R G )
7 opex 
 |-  <. F , G >. e. _V
8 7 a1i 
 |-  ( ph -> <. F , G >. e. _V )
9 1 2 3 4 8 prcofvala 
 |-  ( ph -> ( <. D , E >. -o.F <. F , G >. ) = <. ( k e. B |-> ( k o.func <. F , G >. ) ) , ( k e. B , l e. B |-> ( a e. ( k N l ) |-> ( a o. ( 1st ` <. F , G >. ) ) ) ) >. )
10 5 brrelex12i 
 |-  ( F R G -> ( F e. _V /\ G e. _V ) )
11 op1stg 
 |-  ( ( F e. _V /\ G e. _V ) -> ( 1st ` <. F , G >. ) = F )
12 6 10 11 3syl 
 |-  ( ph -> ( 1st ` <. F , G >. ) = F )
13 12 coeq2d 
 |-  ( ph -> ( a o. ( 1st ` <. F , G >. ) ) = ( a o. F ) )
14 13 mpteq2dv 
 |-  ( ph -> ( a e. ( k N l ) |-> ( a o. ( 1st ` <. F , G >. ) ) ) = ( a e. ( k N l ) |-> ( a o. F ) ) )
15 14 mpoeq3dv 
 |-  ( ph -> ( k e. B , l e. B |-> ( a e. ( k N l ) |-> ( a o. ( 1st ` <. F , G >. ) ) ) ) = ( k e. B , l e. B |-> ( a e. ( k N l ) |-> ( a o. F ) ) ) )
16 15 opeq2d 
 |-  ( ph -> <. ( k e. B |-> ( k o.func <. F , G >. ) ) , ( k e. B , l e. B |-> ( a e. ( k N l ) |-> ( a o. ( 1st ` <. F , G >. ) ) ) ) >. = <. ( k e. B |-> ( k o.func <. F , G >. ) ) , ( k e. B , l e. B |-> ( a e. ( k N l ) |-> ( a o. F ) ) ) >. )
17 9 16 eqtrd 
 |-  ( ph -> ( <. D , E >. -o.F <. F , G >. ) = <. ( k e. B |-> ( k o.func <. F , G >. ) ) , ( k e. B , l e. B |-> ( a e. ( k N l ) |-> ( a o. F ) ) ) >. )