resfval

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

	Ref	Expression
Hypotheses	resfval.c	$⊢ φ \to F \in V$
	resfval.d	$⊢ φ \to H \in W$
Assertion	resfval	$⊢ φ \to F ↾_{f} H = ⟨{1^{st} (F) ↾}_{dom dom H}, (x \in dom H ⟼ {2^{nd} (F) (x) ↾}_{H (x)})⟩$

Proof

Step	Hyp	Ref	Expression
1		resfval.c	$⊢ φ \to F \in V$
2		resfval.d	$⊢ φ \to H \in W$
3		df-resf	$⊢ ↾_{f} = (f \in V, h \in V ⟼ ⟨{1^{st} (f) ↾}_{dom dom h}, (x \in dom h ⟼ {2^{nd} (f) (x) ↾}_{h (x)})⟩)$
4	3	a1i	$⊢ φ \to ↾_{f} = (f \in V, h \in V ⟼ ⟨{1^{st} (f) ↾}_{dom dom h}, (x \in dom h ⟼ {2^{nd} (f) (x) ↾}_{h (x)})⟩)$
5		simprl	$⊢ (φ \land (f = F \land h = H)) \to f = F$
6	5	fveq2d	$⊢ (φ \land (f = F \land h = H)) \to 1^{st} (f) = 1^{st} (F)$
7		simprr	$⊢ (φ \land (f = F \land h = H)) \to h = H$
8	7	dmeqd	$⊢ (φ \land (f = F \land h = H)) \to dom h = dom H$
9	8	dmeqd	$⊢ (φ \land (f = F \land h = H)) \to dom dom h = dom dom H$
10	6 9	reseq12d	$⊢ (φ \land (f = F \land h = H)) \to {1^{st} (f) ↾}_{dom dom h} = {1^{st} (F) ↾}_{dom dom H}$
11	5	fveq2d	$⊢ (φ \land (f = F \land h = H)) \to 2^{nd} (f) = 2^{nd} (F)$
12	11	fveq1d	$⊢ (φ \land (f = F \land h = H)) \to 2^{nd} (f) (x) = 2^{nd} (F) (x)$
13	7	fveq1d	$⊢ (φ \land (f = F \land h = H)) \to h (x) = H (x)$
14	12 13	reseq12d	$⊢ (φ \land (f = F \land h = H)) \to {2^{nd} (f) (x) ↾}_{h (x)} = {2^{nd} (F) (x) ↾}_{H (x)}$
15	8 14	mpteq12dv	$⊢ (φ \land (f = F \land h = H)) \to (x \in dom h ⟼ {2^{nd} (f) (x) ↾}_{h (x)}) = (x \in dom H ⟼ {2^{nd} (F) (x) ↾}_{H (x)})$
16	10 15	opeq12d	$⊢ (φ \land (f = F \land h = H)) \to ⟨{1^{st} (f) ↾}_{dom dom h}, (x \in dom h ⟼ {2^{nd} (f) (x) ↾}_{h (x)})⟩ = ⟨{1^{st} (F) ↾}_{dom dom H}, (x \in dom H ⟼ {2^{nd} (F) (x) ↾}_{H (x)})⟩$
17	1	elexd	$⊢ φ \to F \in V$
18	2	elexd	$⊢ φ \to H \in V$
19		opex	$⊢ ⟨{1^{st} (F) ↾}_{dom dom H}, (x \in dom H ⟼ {2^{nd} (F) (x) ↾}_{H (x)})⟩ \in V$
20	19	a1i	$⊢ φ \to ⟨{1^{st} (F) ↾}_{dom dom H}, (x \in dom H ⟼ {2^{nd} (F) (x) ↾}_{H (x)})⟩ \in V$
21	4 16 17 18 20	ovmpod	$⊢ φ \to F ↾_{f} H = ⟨{1^{st} (F) ↾}_{dom dom H}, (x \in dom H ⟼ {2^{nd} (F) (x) ↾}_{H (x)})⟩$

Metamath Proof Explorer

Theorem resfval

Proof