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 φFV
resf1st.h φHW
resf1st.s φHFnS×S
Assertion resf1st φ1stFfH=1stFS

Proof

Step Hyp Ref Expression
1 resf1st.f φFV
2 resf1st.h φHW
3 resf1st.s φHFnS×S
4 1 2 resfval φFfH=1stFdomdomHzdomH2ndFzHz
5 4 fveq2d φ1stFfH=1st1stFdomdomHzdomH2ndFzHz
6 fvex 1stFV
7 6 resex 1stFdomdomHV
8 dmexg HWdomHV
9 mptexg domHVzdomH2ndFzHzV
10 2 8 9 3syl φzdomH2ndFzHzV
11 op1stg 1stFdomdomHVzdomH2ndFzHzV1st1stFdomdomHzdomH2ndFzHz=1stFdomdomH
12 7 10 11 sylancr φ1st1stFdomdomHzdomH2ndFzHz=1stFdomdomH
13 3 fndmd φdomH=S×S
14 13 dmeqd φdomdomH=domS×S
15 dmxpid domS×S=S
16 14 15 eqtrdi φdomdomH=S
17 16 reseq2d φ1stFdomdomH=1stFS
18 5 12 17 3eqtrd φ1stFfH=1stFS