Theorem resf1st

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

	Ref	Expression
Hypotheses	resf1st.f	$$⊢\phi \to F\in V$$
	resf1st.h	$$⊢\phi \to H\in W$$
	resf1st.s	$$⊢\phi \to HFn\left(S\times S\right)$$
Assertion	resf1st	$$⊢\phi \to 1^{st}\left(F{\upharpoonright }_{f}H\right)={1^{st}\left(F\right)\upharpoonright }_S$$

Proof

Step	Hyp	Ref	Expression
1		resf1st.f	$$⊢\phi \to F\in V$$
2		resf1st.h	$$⊢\phi \to H\in W$$
3		resf1st.s	$$⊢\phi \to HFn\left(S\times S\right)$$
4	1 2	resfval	$$⊢\phi \to F{\upharpoonright }_{f}H=⟨{1^{st}\left(F\right)\upharpoonright }_{\mathrm{dom}\mathrm{dom}H},\left(z\in \mathrm{dom}H⟼{2^{nd}\left(F\right)\left(z\right)\upharpoonright }_{H\left(z\right)}\right)⟩$$
5	4	fveq2d	$$⊢\phi \to 1^{st}\left(F{\upharpoonright }_{f}H\right)=1^{st}\left(⟨{1^{st}\left(F\right)\upharpoonright }_{\mathrm{dom}\mathrm{dom}H},\left(z\in \mathrm{dom}H⟼{2^{nd}\left(F\right)\left(z\right)\upharpoonright }_{H\left(z\right)}\right)⟩\right)$$
6		fvex	$$⊢1^{st}\left(F\right)\in \mathrm{V}$$
7	6	resex	$$⊢{1^{st}\left(F\right)\upharpoonright }_{\mathrm{dom}\mathrm{dom}H}\in \mathrm{V}$$
8		dmexg	$$⊢H\in W\to \mathrm{dom}H\in \mathrm{V}$$
9		mptexg	$$⊢\mathrm{dom}H\in \mathrm{V}\to \left(z\in \mathrm{dom}H⟼{2^{nd}\left(F\right)\left(z\right)\upharpoonright }_{H\left(z\right)}\right)\in \mathrm{V}$$
10	2 8 9	3syl	$$⊢\phi \to \left(z\in \mathrm{dom}H⟼{2^{nd}\left(F\right)\left(z\right)\upharpoonright }_{H\left(z\right)}\right)\in \mathrm{V}$$
11		op1stg	$$⊢\left({1^{st}\left(F\right)\upharpoonright }_{\mathrm{dom}\mathrm{dom}H}\in \mathrm{V}\wedge \left(z\in \mathrm{dom}H⟼{2^{nd}\left(F\right)\left(z\right)\upharpoonright }_{H\left(z\right)}\right)\in \mathrm{V}\right)\to 1^{st}\left(⟨{1^{st}\left(F\right)\upharpoonright }_{\mathrm{dom}\mathrm{dom}H},\left(z\in \mathrm{dom}H⟼{2^{nd}\left(F\right)\left(z\right)\upharpoonright }_{H\left(z\right)}\right)⟩\right)={1^{st}\left(F\right)\upharpoonright }_{\mathrm{dom}\mathrm{dom}H}$$
12	7 10 11	sylancr	$$⊢\phi \to 1^{st}\left(⟨{1^{st}\left(F\right)\upharpoonright }_{\mathrm{dom}\mathrm{dom}H},\left(z\in \mathrm{dom}H⟼{2^{nd}\left(F\right)\left(z\right)\upharpoonright }_{H\left(z\right)}\right)⟩\right)={1^{st}\left(F\right)\upharpoonright }_{\mathrm{dom}\mathrm{dom}H}$$
13	3	fndmd	$$⊢\phi \to \mathrm{dom}H=S\times S$$
14	13	dmeqd	$$⊢\phi \to \mathrm{dom}\mathrm{dom}H=\mathrm{dom}\left(S\times S\right)$$
15		dmxpid	$$⊢\mathrm{dom}\left(S\times S\right)=S$$
16	14 15	eqtrdi	$$⊢\phi \to \mathrm{dom}\mathrm{dom}H=S$$
17	16	reseq2d	$$⊢\phi \to {1^{st}\left(F\right)\upharpoonright }_{\mathrm{dom}\mathrm{dom}H}={1^{st}\left(F\right)\upharpoonright }_S$$
18	5 12 17	3eqtrd	$$⊢\phi \to 1^{st}\left(F{\upharpoonright }_{f}H\right)={1^{st}\left(F\right)\upharpoonright }_S$$