Metamath Proof Explorer

Theorem prcof2a

Description: The morphism part of the pre-composition functor. (Contributed by Zhi Wang, 3-Nov-2025)

Ref Expression
Hypotheses prcof2a.n 
|- N = ( D Nat E )
prcof2a.k 
|- ( ph -> K e. ( D Func E ) )
prcof2a.l 
|- ( ph -> L e. ( D Func E ) )
prcof2a.p 
|- ( ph -> ( 2nd ` ( <. D , E >. -o.F F ) ) = P )
prcof2a.f 
|- ( ph -> F e. U )
Assertion prcof2a 
|- ( ph -> ( K P L ) = ( a e. ( K N L ) |-> ( a o. ( 1st ` F ) ) ) )

Proof

Step Hyp Ref Expression
1 prcof2a.n 
 |-  N = ( D Nat E )
2 prcof2a.k 
 |-  ( ph -> K e. ( D Func E ) )
3 prcof2a.l 
 |-  ( ph -> L e. ( D Func E ) )
4 prcof2a.p 
 |-  ( ph -> ( 2nd ` ( <. D , E >. -o.F F ) ) = P )
5 prcof2a.f 
 |-  ( ph -> F e. U )
6 eqid 
 |-  ( D Func E ) = ( D Func E )
7 2 func1st2nd 
 |-  ( ph -> ( 1st ` K ) ( D Func E ) ( 2nd ` K ) )
8 7 funcrcl2 
 |-  ( ph -> D e. Cat )
9 7 funcrcl3 
 |-  ( ph -> E e. Cat )
10 6 1 8 9 5 prcofvala 
 |-  ( ph -> ( <. D , E >. -o.F F ) = <. ( k e. ( D Func E ) |-> ( k o.func F ) ) , ( k e. ( D Func E ) , l e. ( D Func E ) |-> ( a e. ( k N l ) |-> ( a o. ( 1st ` F ) ) ) ) >. )
11 10 fveq2d 
 |-  ( ph -> ( 2nd ` ( <. D , E >. -o.F F ) ) = ( 2nd ` <. ( k e. ( D Func E ) |-> ( k o.func F ) ) , ( k e. ( D Func E ) , l e. ( D Func E ) |-> ( a e. ( k N l ) |-> ( a o. ( 1st ` F ) ) ) ) >. ) )
12 ovex 
 |-  ( D Func E ) e. _V
13 12 mptex 
 |-  ( k e. ( D Func E ) |-> ( k o.func F ) ) e. _V
14 12 12 mpoex 
 |-  ( k e. ( D Func E ) , l e. ( D Func E ) |-> ( a e. ( k N l ) |-> ( a o. ( 1st ` F ) ) ) ) e. _V
15 13 14 op2nd 
 |-  ( 2nd ` <. ( k e. ( D Func E ) |-> ( k o.func F ) ) , ( k e. ( D Func E ) , l e. ( D Func E ) |-> ( a e. ( k N l ) |-> ( a o. ( 1st ` F ) ) ) ) >. ) = ( k e. ( D Func E ) , l e. ( D Func E ) |-> ( a e. ( k N l ) |-> ( a o. ( 1st ` F ) ) ) )
16 11 15 eqtrdi 
 |-  ( ph -> ( 2nd ` ( <. D , E >. -o.F F ) ) = ( k e. ( D Func E ) , l e. ( D Func E ) |-> ( a e. ( k N l ) |-> ( a o. ( 1st ` F ) ) ) ) )
17 4 16 eqtr3d 
 |-  ( ph -> P = ( k e. ( D Func E ) , l e. ( D Func E ) |-> ( a e. ( k N l ) |-> ( a o. ( 1st ` F ) ) ) ) )
18 simprl 
 |-  ( ( ph /\ ( k = K /\ l = L ) ) -> k = K )
19 simprr 
 |-  ( ( ph /\ ( k = K /\ l = L ) ) -> l = L )
20 18 19 oveq12d 
 |-  ( ( ph /\ ( k = K /\ l = L ) ) -> ( k N l ) = ( K N L ) )
21 20 mpteq1d 
 |-  ( ( ph /\ ( k = K /\ l = L ) ) -> ( a e. ( k N l ) |-> ( a o. ( 1st ` F ) ) ) = ( a e. ( K N L ) |-> ( a o. ( 1st ` F ) ) ) )
22 ovex 
 |-  ( K N L ) e. _V
23 22 mptex 
 |-  ( a e. ( K N L ) |-> ( a o. ( 1st ` F ) ) ) e. _V
24 23 a1i 
 |-  ( ph -> ( a e. ( K N L ) |-> ( a o. ( 1st ` F ) ) ) e. _V )
25 17 21 2 3 24 ovmpod 
 |-  ( ph -> ( K P L ) = ( a e. ( K N L ) |-> ( a o. ( 1st ` F ) ) ) )