Metamath Proof Explorer

Theorem rescofuf

Description: The restriction of functor composition is a function from product functor space to functor space. (Contributed by Zhi Wang, 25-Sep-2025)

Ref Expression
Assertion rescofuf 
|- ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) : ( ( D Func E ) X. ( C Func D ) ) --> ( C Func E )

Proof

Step Hyp Ref Expression
1 vex 
 |-  g e. _V
2 vex 
 |-  f e. _V
3 opex 
 |-  <. ( ( 1st ` g ) o. ( 1st ` f ) ) , ( x e. dom dom ( 2nd ` f ) , y e. dom dom ( 2nd ` f ) |-> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) ) >. e. _V
4 df-cofu 
 |-  o.func = ( g e. _V , f e. _V |-> <. ( ( 1st ` g ) o. ( 1st ` f ) ) , ( x e. dom dom ( 2nd ` f ) , y e. dom dom ( 2nd ` f ) |-> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) ) >. )
5 4 ovmpt4g 
 |-  ( ( g e. _V /\ f e. _V /\ <. ( ( 1st ` g ) o. ( 1st ` f ) ) , ( x e. dom dom ( 2nd ` f ) , y e. dom dom ( 2nd ` f ) |-> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) ) >. e. _V ) -> ( g o.func f ) = <. ( ( 1st ` g ) o. ( 1st ` f ) ) , ( x e. dom dom ( 2nd ` f ) , y e. dom dom ( 2nd ` f ) |-> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) ) >. )
6 1 2 3 5 mp3an 
 |-  ( g o.func f ) = <. ( ( 1st ` g ) o. ( 1st ` f ) ) , ( x e. dom dom ( 2nd ` f ) , y e. dom dom ( 2nd ` f ) |-> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) ) >.
7 simpr 
 |-  ( ( g e. ( D Func E ) /\ f e. ( C Func D ) ) -> f e. ( C Func D ) )
8 simpl 
 |-  ( ( g e. ( D Func E ) /\ f e. ( C Func D ) ) -> g e. ( D Func E ) )
9 7 8 cofucl 
 |-  ( ( g e. ( D Func E ) /\ f e. ( C Func D ) ) -> ( g o.func f ) e. ( C Func E ) )
10 6 9 eqeltrrid 
 |-  ( ( g e. ( D Func E ) /\ f e. ( C Func D ) ) -> <. ( ( 1st ` g ) o. ( 1st ` f ) ) , ( x e. dom dom ( 2nd ` f ) , y e. dom dom ( 2nd ` f ) |-> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) ) >. e. ( C Func E ) )
11 10 rgen2 
 |-  A. g e. ( D Func E ) A. f e. ( C Func D ) <. ( ( 1st ` g ) o. ( 1st ` f ) ) , ( x e. dom dom ( 2nd ` f ) , y e. dom dom ( 2nd ` f ) |-> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) ) >. e. ( C Func E )
12 4 reseq1i 
 |-  ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) = ( ( g e. _V , f e. _V |-> <. ( ( 1st ` g ) o. ( 1st ` f ) ) , ( x e. dom dom ( 2nd ` f ) , y e. dom dom ( 2nd ` f ) |-> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) ) >. ) |` ( ( D Func E ) X. ( C Func D ) ) )
13 ssv 
 |-  ( D Func E ) C_ _V
14 ssv 
 |-  ( C Func D ) C_ _V
15 resmpo 
 |-  ( ( ( D Func E ) C_ _V /\ ( C Func D ) C_ _V ) -> ( ( g e. _V , f e. _V |-> <. ( ( 1st ` g ) o. ( 1st ` f ) ) , ( x e. dom dom ( 2nd ` f ) , y e. dom dom ( 2nd ` f ) |-> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) ) >. ) |` ( ( D Func E ) X. ( C Func D ) ) ) = ( g e. ( D Func E ) , f e. ( C Func D ) |-> <. ( ( 1st ` g ) o. ( 1st ` f ) ) , ( x e. dom dom ( 2nd ` f ) , y e. dom dom ( 2nd ` f ) |-> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) ) >. ) )
16 13 14 15 mp2an 
 |-  ( ( g e. _V , f e. _V |-> <. ( ( 1st ` g ) o. ( 1st ` f ) ) , ( x e. dom dom ( 2nd ` f ) , y e. dom dom ( 2nd ` f ) |-> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) ) >. ) |` ( ( D Func E ) X. ( C Func D ) ) ) = ( g e. ( D Func E ) , f e. ( C Func D ) |-> <. ( ( 1st ` g ) o. ( 1st ` f ) ) , ( x e. dom dom ( 2nd ` f ) , y e. dom dom ( 2nd ` f ) |-> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) ) >. )
17 12 16 eqtri 
 |-  ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) = ( g e. ( D Func E ) , f e. ( C Func D ) |-> <. ( ( 1st ` g ) o. ( 1st ` f ) ) , ( x e. dom dom ( 2nd ` f ) , y e. dom dom ( 2nd ` f ) |-> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) ) >. )
18 17 fmpo 
 |-  ( A. g e. ( D Func E ) A. f e. ( C Func D ) <. ( ( 1st ` g ) o. ( 1st ` f ) ) , ( x e. dom dom ( 2nd ` f ) , y e. dom dom ( 2nd ` f ) |-> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) ) >. e. ( C Func E ) <-> ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) : ( ( D Func E ) X. ( C Func D ) ) --> ( C Func E ) )
19 11 18 mpbi 
 |-  ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) : ( ( D Func E ) X. ( C Func D ) ) --> ( C Func E )