resf2nd

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

	Ref	Expression
Hypotheses	resf1st.f	$⊢ φ \to F \in V$
	resf1st.h	$⊢ φ \to H \in W$
	resf1st.s	$⊢ φ \to H Fn (S \times S)$
	resf2nd.x	$⊢ φ \to X \in S$
	resf2nd.y	$⊢ φ \to Y \in S$
Assertion	resf2nd	$⊢ φ \to X 2^{nd} (F ↾_{f} H) Y = {(X 2^{nd} (F) Y) ↾}_{(X H Y)}$

Proof

Step	Hyp	Ref	Expression
1		resf1st.f	$⊢ φ \to F \in V$
2		resf1st.h	$⊢ φ \to H \in W$
3		resf1st.s	$⊢ φ \to H Fn (S \times S)$
4		resf2nd.x	$⊢ φ \to X \in S$
5		resf2nd.y	$⊢ φ \to Y \in S$
6		df-ov	$⊢ X 2^{nd} (F ↾_{f} H) Y = 2^{nd} (F ↾_{f} H) (⟨X, Y⟩)$
7	1 2	resfval	$⊢ φ \to F ↾_{f} H = ⟨{1^{st} (F) ↾}_{dom dom H}, (z \in dom H ⟼ {2^{nd} (F) (z) ↾}_{H (z)})⟩$
8	7	fveq2d	$⊢ φ \to 2^{nd} (F ↾_{f} H) = 2^{nd} (⟨{1^{st} (F) ↾}_{dom dom H}, (z \in dom H ⟼ {2^{nd} (F) (z) ↾}_{H (z)})⟩)$
9		fvex	$⊢ 1^{st} (F) \in V$
10	9	resex	$⊢ {1^{st} (F) ↾}_{dom dom H} \in V$
11		dmexg	$⊢ H \in W \to dom H \in V$
12		mptexg	$⊢ dom H \in V \to (z \in dom H ⟼ {2^{nd} (F) (z) ↾}_{H (z)}) \in V$
13	2 11 12	3syl	$⊢ φ \to (z \in dom H ⟼ {2^{nd} (F) (z) ↾}_{H (z)}) \in V$
14		op2ndg	$⊢ ({1^{st} (F) ↾}_{dom dom H} \in V \land (z \in dom H ⟼ {2^{nd} (F) (z) ↾}_{H (z)}) \in V) \to 2^{nd} (⟨{1^{st} (F) ↾}_{dom dom H}, (z \in dom H ⟼ {2^{nd} (F) (z) ↾}_{H (z)})⟩) = (z \in dom H ⟼ {2^{nd} (F) (z) ↾}_{H (z)})$
15	10 13 14	sylancr	$⊢ φ \to 2^{nd} (⟨{1^{st} (F) ↾}_{dom dom H}, (z \in dom H ⟼ {2^{nd} (F) (z) ↾}_{H (z)})⟩) = (z \in dom H ⟼ {2^{nd} (F) (z) ↾}_{H (z)})$
16	8 15	eqtrd	$⊢ φ \to 2^{nd} (F ↾_{f} H) = (z \in dom H ⟼ {2^{nd} (F) (z) ↾}_{H (z)})$
17		simpr	$⊢ (φ \land z = ⟨X, Y⟩) \to z = ⟨X, Y⟩$
18	17	fveq2d	$⊢ (φ \land z = ⟨X, Y⟩) \to 2^{nd} (F) (z) = 2^{nd} (F) (⟨X, Y⟩)$
19		df-ov	$⊢ X 2^{nd} (F) Y = 2^{nd} (F) (⟨X, Y⟩)$
20	18 19	eqtr4di	$⊢ (φ \land z = ⟨X, Y⟩) \to 2^{nd} (F) (z) = X 2^{nd} (F) Y$
21	17	fveq2d	$⊢ (φ \land z = ⟨X, Y⟩) \to H (z) = H (⟨X, Y⟩)$
22		df-ov	$⊢ X H Y = H (⟨X, Y⟩)$
23	21 22	eqtr4di	$⊢ (φ \land z = ⟨X, Y⟩) \to H (z) = X H Y$
24	20 23	reseq12d	$⊢ (φ \land z = ⟨X, Y⟩) \to {2^{nd} (F) (z) ↾}_{H (z)} = {(X 2^{nd} (F) Y) ↾}_{(X H Y)}$
25	4 5	opelxpd	$⊢ φ \to ⟨X, Y⟩ \in (S \times S)$
26	3	fndmd	$⊢ φ \to dom H = S \times S$
27	25 26	eleqtrrd	$⊢ φ \to ⟨X, Y⟩ \in dom H$
28		ovex	$⊢ X 2^{nd} (F) Y \in V$
29	28	resex	$⊢ {(X 2^{nd} (F) Y) ↾}_{(X H Y)} \in V$
30	29	a1i	$⊢ φ \to {(X 2^{nd} (F) Y) ↾}_{(X H Y)} \in V$
31	16 24 27 30	fvmptd	$⊢ φ \to 2^{nd} (F ↾_{f} H) (⟨X, Y⟩) = {(X 2^{nd} (F) Y) ↾}_{(X H Y)}$
32	6 31	syl5eq	$⊢ φ \to X 2^{nd} (F ↾_{f} H) Y = {(X 2^{nd} (F) Y) ↾}_{(X H Y)}$

Metamath Proof Explorer

Theorem resf2nd

Proof