Metamath Proof Explorer

Theorem prcofvala

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 )
prcofvala.f 
|- ( ph -> F e. U )
Assertion prcofvala 
|- ( ph -> ( <. D , E >. -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 prcofvala.d 
 |-  ( ph -> D e. V )
4 prcofvala.e 
 |-  ( ph -> E e. W )
5 prcofvala.f 
 |-  ( ph -> F e. U )
6 opex 
 |-  <. D , E >. e. _V
7 6 a1i 
 |-  ( ph -> <. D , E >. e. _V )
8 op1stg 
 |-  ( ( D e. V /\ E e. W ) -> ( 1st ` <. D , E >. ) = D )
9 3 4 8 syl2anc 
 |-  ( ph -> ( 1st ` <. D , E >. ) = D )
10 op2ndg 
 |-  ( ( D e. V /\ E e. W ) -> ( 2nd ` <. D , E >. ) = E )
11 3 4 10 syl2anc 
 |-  ( ph -> ( 2nd ` <. D , E >. ) = E )
12 1 2 5 7 9 11 prcofvalg 
 |-  ( ph -> ( <. D , E >. -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 ) ) ) ) >. )