Metamath Proof Explorer

Theorem prcof2

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 ) )
prcof2.p 
|- ( ph -> ( 2nd ` ( <. D , E >. -o.F <. F , G >. ) ) = P )
prcof2.r 
|- Rel R
prcof2.f 
|- ( ph -> F R G )
Assertion prcof2 
|- ( ph -> ( K P L ) = ( a e. ( K N L ) |-> ( a o. 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 prcof2.p 
 |-  ( ph -> ( 2nd ` ( <. D , E >. -o.F <. F , G >. ) ) = P )
5 prcof2.r 
 |-  Rel R
6 prcof2.f 
 |-  ( ph -> F R G )
7 eqid 
 |-  ( D Func E ) = ( D Func E )
8 2 func1st2nd 
 |-  ( ph -> ( 1st ` K ) ( D Func E ) ( 2nd ` K ) )
9 8 funcrcl2 
 |-  ( ph -> D e. Cat )
10 8 funcrcl3 
 |-  ( ph -> E e. Cat )
11 7 1 9 10 5 6 prcofval 
 |-  ( ph -> ( <. D , E >. -o.F <. F , G >. ) = <. ( k e. ( D Func E ) |-> ( k o.func <. F , G >. ) ) , ( k e. ( D Func E ) , l e. ( D Func E ) |-> ( a e. ( k N l ) |-> ( a o. F ) ) ) >. )
12 11 fveq2d 
 |-  ( ph -> ( 2nd ` ( <. D , E >. -o.F <. F , G >. ) ) = ( 2nd ` <. ( k e. ( D Func E ) |-> ( k o.func <. F , G >. ) ) , ( k e. ( D Func E ) , l e. ( D Func E ) |-> ( a e. ( k N l ) |-> ( a o. F ) ) ) >. ) )
13 ovex 
 |-  ( D Func E ) e. _V
14 13 mptex 
 |-  ( k e. ( D Func E ) |-> ( k o.func <. F , G >. ) ) e. _V
15 13 13 mpoex 
 |-  ( k e. ( D Func E ) , l e. ( D Func E ) |-> ( a e. ( k N l ) |-> ( a o. F ) ) ) e. _V
16 14 15 op2nd 
 |-  ( 2nd ` <. ( k e. ( D Func E ) |-> ( k o.func <. F , G >. ) ) , ( k e. ( D Func E ) , l e. ( D Func E ) |-> ( a e. ( k N l ) |-> ( a o. F ) ) ) >. ) = ( k e. ( D Func E ) , l e. ( D Func E ) |-> ( a e. ( k N l ) |-> ( a o. F ) ) )
17 12 16 eqtrdi 
 |-  ( ph -> ( 2nd ` ( <. D , E >. -o.F <. F , G >. ) ) = ( k e. ( D Func E ) , l e. ( D Func E ) |-> ( a e. ( k N l ) |-> ( a o. F ) ) ) )
18 4 17 eqtr3d 
 |-  ( ph -> P = ( k e. ( D Func E ) , l e. ( D Func E ) |-> ( a e. ( k N l ) |-> ( a o. F ) ) ) )
19 simprl 
 |-  ( ( ph /\ ( k = K /\ l = L ) ) -> k = K )
20 simprr 
 |-  ( ( ph /\ ( k = K /\ l = L ) ) -> l = L )
21 19 20 oveq12d 
 |-  ( ( ph /\ ( k = K /\ l = L ) ) -> ( k N l ) = ( K N L ) )
22 21 mpteq1d 
 |-  ( ( ph /\ ( k = K /\ l = L ) ) -> ( a e. ( k N l ) |-> ( a o. F ) ) = ( a e. ( K N L ) |-> ( a o. F ) ) )
23 ovex 
 |-  ( K N L ) e. _V
24 23 mptex 
 |-  ( a e. ( K N L ) |-> ( a o. F ) ) e. _V
25 24 a1i 
 |-  ( ph -> ( a e. ( K N L ) |-> ( a o. F ) ) e. _V )
26 18 22 2 3 25 ovmpod 
 |-  ( ph -> ( K P L ) = ( a e. ( K N L ) |-> ( a o. F ) ) )