Metamath Proof Explorer

Theorem resf2nd

Description: Value of the functor restriction operator on morphisms. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses resf1st.f 
|- ( ph -> F e. V )
resf1st.h 
|- ( ph -> H e. W )
resf1st.s 
|- ( ph -> H Fn ( S X. S ) )
resf2nd.x 
|- ( ph -> X e. S )
resf2nd.y 
|- ( ph -> Y e. S )
Assertion resf2nd 
|- ( ph -> ( X ( 2nd ` ( F |`f H ) ) Y ) = ( ( X ( 2nd ` F ) Y ) |` ( X H Y ) ) )

Proof

Step Hyp Ref Expression
1 resf1st.f 
 |-  ( ph -> F e. V )
2 resf1st.h 
 |-  ( ph -> H e. W )
3 resf1st.s 
 |-  ( ph -> H Fn ( S X. S ) )
4 resf2nd.x 
 |-  ( ph -> X e. S )
5 resf2nd.y 
 |-  ( ph -> Y e. S )
6 df-ov 
 |-  ( X ( 2nd ` ( F |`f H ) ) Y ) = ( ( 2nd ` ( F |`f H ) ) ` <. X , Y >. )
7 1 2 resfval 
 |-  ( ph -> ( F |`f H ) = <. ( ( 1st ` F ) |` dom dom H ) , ( z e. dom H |-> ( ( ( 2nd ` F ) ` z ) |` ( H ` z ) ) ) >. )
8 7 fveq2d 
 |-  ( ph -> ( 2nd ` ( F |`f H ) ) = ( 2nd ` <. ( ( 1st ` F ) |` dom dom H ) , ( z e. dom H |-> ( ( ( 2nd ` F ) ` z ) |` ( H ` z ) ) ) >. ) )
9 fvex 
 |-  ( 1st ` F ) e. _V
10 9 resex 
 |-  ( ( 1st ` F ) |` dom dom H ) e. _V
11 dmexg 
 |-  ( H e. W -> dom H e. _V )
12 mptexg 
 |-  ( dom H e. _V -> ( z e. dom H |-> ( ( ( 2nd ` F ) ` z ) |` ( H ` z ) ) ) e. _V )
13 2 11 12 3syl 
 |-  ( ph -> ( z e. dom H |-> ( ( ( 2nd ` F ) ` z ) |` ( H ` z ) ) ) e. _V )
14 op2ndg 
 |-  ( ( ( ( 1st ` F ) |` dom dom H ) e. _V /\ ( z e. dom H |-> ( ( ( 2nd ` F ) ` z ) |` ( H ` z ) ) ) e. _V ) -> ( 2nd ` <. ( ( 1st ` F ) |` dom dom H ) , ( z e. dom H |-> ( ( ( 2nd ` F ) ` z ) |` ( H ` z ) ) ) >. ) = ( z e. dom H |-> ( ( ( 2nd ` F ) ` z ) |` ( H ` z ) ) ) )
15 10 13 14 sylancr 
 |-  ( ph -> ( 2nd ` <. ( ( 1st ` F ) |` dom dom H ) , ( z e. dom H |-> ( ( ( 2nd ` F ) ` z ) |` ( H ` z ) ) ) >. ) = ( z e. dom H |-> ( ( ( 2nd ` F ) ` z ) |` ( H ` z ) ) ) )
16 8 15 eqtrd 
 |-  ( ph -> ( 2nd ` ( F |`f H ) ) = ( z e. dom H |-> ( ( ( 2nd ` F ) ` z ) |` ( H ` z ) ) ) )
17 simpr 
 |-  ( ( ph /\ z = <. X , Y >. ) -> z = <. X , Y >. )
18 17 fveq2d 
 |-  ( ( ph /\ z = <. X , Y >. ) -> ( ( 2nd ` F ) ` z ) = ( ( 2nd ` F ) ` <. X , Y >. ) )
19 df-ov 
 |-  ( X ( 2nd ` F ) Y ) = ( ( 2nd ` F ) ` <. X , Y >. )
20 18 19 eqtr4di 
 |-  ( ( ph /\ z = <. X , Y >. ) -> ( ( 2nd ` F ) ` z ) = ( X ( 2nd ` F ) Y ) )
21 17 fveq2d 
 |-  ( ( ph /\ z = <. X , Y >. ) -> ( H ` z ) = ( H ` <. X , Y >. ) )
22 df-ov 
 |-  ( X H Y ) = ( H ` <. X , Y >. )
23 21 22 eqtr4di 
 |-  ( ( ph /\ z = <. X , Y >. ) -> ( H ` z ) = ( X H Y ) )
24 20 23 reseq12d 
 |-  ( ( ph /\ z = <. X , Y >. ) -> ( ( ( 2nd ` F ) ` z ) |` ( H ` z ) ) = ( ( X ( 2nd ` F ) Y ) |` ( X H Y ) ) )
25 4 5 opelxpd 
 |-  ( ph -> <. X , Y >. e. ( S X. S ) )
26 3 fndmd 
 |-  ( ph -> dom H = ( S X. S ) )
27 25 26 eleqtrrd 
 |-  ( ph -> <. X , Y >. e. dom H )
28 ovex 
 |-  ( X ( 2nd ` F ) Y ) e. _V
29 28 resex 
 |-  ( ( X ( 2nd ` F ) Y ) |` ( X H Y ) ) e. _V
30 29 a1i 
 |-  ( ph -> ( ( X ( 2nd ` F ) Y ) |` ( X H Y ) ) e. _V )
31 16 24 27 30 fvmptd 
 |-  ( ph -> ( ( 2nd ` ( F |`f H ) ) ` <. X , Y >. ) = ( ( X ( 2nd ` F ) Y ) |` ( X H Y ) ) )
32 6 31 syl5eq 
 |-  ( ph -> ( X ( 2nd ` ( F |`f H ) ) Y ) = ( ( X ( 2nd ` F ) Y ) |` ( X H Y ) ) )