Metamath Proof Explorer

Theorem resf1st

Description: Value of the functor restriction operator on objects. (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 ) )
Assertion resf1st 
|- ( ph -> ( 1st ` ( F |`f H ) ) = ( ( 1st ` F ) |` S ) )

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 1 2 resfval 
 |-  ( ph -> ( F |`f H ) = <. ( ( 1st ` F ) |` dom dom H ) , ( z e. dom H |-> ( ( ( 2nd ` F ) ` z ) |` ( H ` z ) ) ) >. )
5 4 fveq2d 
 |-  ( ph -> ( 1st ` ( F |`f H ) ) = ( 1st ` <. ( ( 1st ` F ) |` dom dom H ) , ( z e. dom H |-> ( ( ( 2nd ` F ) ` z ) |` ( H ` z ) ) ) >. ) )
6 fvex 
 |-  ( 1st ` F ) e. _V
7 6 resex 
 |-  ( ( 1st ` F ) |` dom dom H ) e. _V
8 dmexg 
 |-  ( H e. W -> dom H e. _V )
9 mptexg 
 |-  ( dom H e. _V -> ( z e. dom H |-> ( ( ( 2nd ` F ) ` z ) |` ( H ` z ) ) ) e. _V )
10 2 8 9 3syl 
 |-  ( ph -> ( z e. dom H |-> ( ( ( 2nd ` F ) ` z ) |` ( H ` z ) ) ) e. _V )
11 op1stg 
 |-  ( ( ( ( 1st ` F ) |` dom dom H ) e. _V /\ ( z e. dom H |-> ( ( ( 2nd ` F ) ` z ) |` ( H ` z ) ) ) e. _V ) -> ( 1st ` <. ( ( 1st ` F ) |` dom dom H ) , ( z e. dom H |-> ( ( ( 2nd ` F ) ` z ) |` ( H ` z ) ) ) >. ) = ( ( 1st ` F ) |` dom dom H ) )
12 7 10 11 sylancr 
 |-  ( ph -> ( 1st ` <. ( ( 1st ` F ) |` dom dom H ) , ( z e. dom H |-> ( ( ( 2nd ` F ) ` z ) |` ( H ` z ) ) ) >. ) = ( ( 1st ` F ) |` dom dom H ) )
13 3 fndmd 
 |-  ( ph -> dom H = ( S X. S ) )
14 13 dmeqd 
 |-  ( ph -> dom dom H = dom ( S X. S ) )
15 dmxpid 
 |-  dom ( S X. S ) = S
16 14 15 eqtrdi 
 |-  ( ph -> dom dom H = S )
17 16 reseq2d 
 |-  ( ph -> ( ( 1st ` F ) |` dom dom H ) = ( ( 1st ` F ) |` S ) )
18 5 12 17 3eqtrd 
 |-  ( ph -> ( 1st ` ( F |`f H ) ) = ( ( 1st ` F ) |` S ) )