msubval

Description: A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	msubffval.v	$⊢ V = mVR (T)$
	msubffval.r	$⊢ R = mREx (T)$
	msubffval.s	$⊢ S = mSubst (T)$
	msubffval.e	$⊢ E = mEx (T)$
	msubffval.o	$⊢ O = mRSubst (T)$
Assertion	msubval	$⊢ (F : A ⟶ R \land A \subseteq V \land X \in E) \to S (F) (X) = ⟨1^{st} (X), O (F) (2^{nd} (X))⟩$

Step	Hyp	Ref	Expression
1		msubffval.v	$⊢ V = mVR (T)$
2		msubffval.r	$⊢ R = mREx (T)$
3		msubffval.s	$⊢ S = mSubst (T)$
4		msubffval.e	$⊢ E = mEx (T)$
5		msubffval.o	$⊢ O = mRSubst (T)$
6	1 2 3 4 5	msubfval	$⊢ (F : A ⟶ R \land A \subseteq V) \to S (F) = (e \in E ⟼ ⟨1^{st} (e), O (F) (2^{nd} (e))⟩)$
7	6	3adant3	$⊢ (F : A ⟶ R \land A \subseteq V \land X \in E) \to S (F) = (e \in E ⟼ ⟨1^{st} (e), O (F) (2^{nd} (e))⟩)$
8		simpr	$⊢ ((F : A ⟶ R \land A \subseteq V \land X \in E) \land e = X) \to e = X$
9	8	fveq2d	$⊢ ((F : A ⟶ R \land A \subseteq V \land X \in E) \land e = X) \to 1^{st} (e) = 1^{st} (X)$
10	8	fveq2d	$⊢ ((F : A ⟶ R \land A \subseteq V \land X \in E) \land e = X) \to 2^{nd} (e) = 2^{nd} (X)$
11	10	fveq2d	$⊢ ((F : A ⟶ R \land A \subseteq V \land X \in E) \land e = X) \to O (F) (2^{nd} (e)) = O (F) (2^{nd} (X))$
12	9 11	opeq12d	$⊢ ((F : A ⟶ R \land A \subseteq V \land X \in E) \land e = X) \to ⟨1^{st} (e), O (F) (2^{nd} (e))⟩ = ⟨1^{st} (X), O (F) (2^{nd} (X))⟩$
13		simp3	$⊢ (F : A ⟶ R \land A \subseteq V \land X \in E) \to X \in E$
14		opex	$⊢ ⟨1^{st} (X), O (F) (2^{nd} (X))⟩ \in V$
15	14	a1i	$⊢ (F : A ⟶ R \land A \subseteq V \land X \in E) \to ⟨1^{st} (X), O (F) (2^{nd} (X))⟩ \in V$
16	7 12 13 15	fvmptd	$⊢ (F : A ⟶ R \land A \subseteq V \land X \in E) \to S (F) (X) = ⟨1^{st} (X), O (F) (2^{nd} (X))⟩$

Metamath Proof Explorer