msubfval

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	msubfval	$⊢ (F : A ⟶ R \land A \subseteq V) \to S (F) = (e \in E ⟼ ⟨1^{st} (e), O (F) (2^{nd} (e))⟩)$

Proof

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	msubffval	$⊢ T \in V \to S = (f \in (R ↑_{𝑝𝑚} V) ⟼ (e \in E ⟼ ⟨1^{st} (e), O (f) (2^{nd} (e))⟩))$
7	6	adantr	$⊢ (T \in V \land (F : A ⟶ R \land A \subseteq V)) \to S = (f \in (R ↑_{𝑝𝑚} V) ⟼ (e \in E ⟼ ⟨1^{st} (e), O (f) (2^{nd} (e))⟩))$
8		simplr	$⊢ (((T \in V \land (F : A ⟶ R \land A \subseteq V)) \land f = F) \land e \in E) \to f = F$
9	8	fveq2d	$⊢ (((T \in V \land (F : A ⟶ R \land A \subseteq V)) \land f = F) \land e \in E) \to O (f) = O (F)$
10	9	fveq1d	$⊢ (((T \in V \land (F : A ⟶ R \land A \subseteq V)) \land f = F) \land e \in E) \to O (f) (2^{nd} (e)) = O (F) (2^{nd} (e))$
11	10	opeq2d	$⊢ (((T \in V \land (F : A ⟶ R \land A \subseteq V)) \land f = F) \land e \in E) \to ⟨1^{st} (e), O (f) (2^{nd} (e))⟩ = ⟨1^{st} (e), O (F) (2^{nd} (e))⟩$
12	11	mpteq2dva	$⊢ ((T \in V \land (F : A ⟶ R \land A \subseteq V)) \land f = F) \to (e \in E ⟼ ⟨1^{st} (e), O (f) (2^{nd} (e))⟩) = (e \in E ⟼ ⟨1^{st} (e), O (F) (2^{nd} (e))⟩)$
13	2	fvexi	$⊢ R \in V$
14	1	fvexi	$⊢ V \in V$
15	13 14	pm3.2i	$⊢ (R \in V \land V \in V)$
16	15	a1i	$⊢ T \in V \to (R \in V \land V \in V)$
17		elpm2r	$⊢ ((R \in V \land V \in V) \land (F : A ⟶ R \land A \subseteq V)) \to F \in (R ↑_{𝑝𝑚} V)$
18	16 17	sylan	$⊢ (T \in V \land (F : A ⟶ R \land A \subseteq V)) \to F \in (R ↑_{𝑝𝑚} V)$
19	4	fvexi	$⊢ E \in V$
20	19	mptex	$⊢ (e \in E ⟼ ⟨1^{st} (e), O (F) (2^{nd} (e))⟩) \in V$
21	20	a1i	$⊢ (T \in V \land (F : A ⟶ R \land A \subseteq V)) \to (e \in E ⟼ ⟨1^{st} (e), O (F) (2^{nd} (e))⟩) \in V$
22	7 12 18 21	fvmptd	$⊢ (T \in V \land (F : A ⟶ R \land A \subseteq V)) \to S (F) = (e \in E ⟼ ⟨1^{st} (e), O (F) (2^{nd} (e))⟩)$
23	22	ex	$⊢ T \in V \to ((F : A ⟶ R \land A \subseteq V) \to S (F) = (e \in E ⟼ ⟨1^{st} (e), O (F) (2^{nd} (e))⟩))$
24		0fv	$⊢ \emptyset (F) = \emptyset$
25		mpt0	$⊢ (e \in \emptyset ⟼ ⟨1^{st} (e), O (F) (2^{nd} (e))⟩) = \emptyset$
26	24 25	eqtr4i	$⊢ \emptyset (F) = (e \in \emptyset ⟼ ⟨1^{st} (e), O (F) (2^{nd} (e))⟩)$
27		fvprc	$⊢ \neg T \in V \to mSubst (T) = \emptyset$
28	3 27	eqtrid	$⊢ \neg T \in V \to S = \emptyset$
29	28	fveq1d	$⊢ \neg T \in V \to S (F) = \emptyset (F)$
30		fvprc	$⊢ \neg T \in V \to mEx (T) = \emptyset$
31	4 30	eqtrid	$⊢ \neg T \in V \to E = \emptyset$
32	31	mpteq1d	$⊢ \neg T \in V \to (e \in E ⟼ ⟨1^{st} (e), O (F) (2^{nd} (e))⟩) = (e \in \emptyset ⟼ ⟨1^{st} (e), O (F) (2^{nd} (e))⟩)$
33	26 29 32	3eqtr4a	$⊢ \neg T \in V \to S (F) = (e \in E ⟼ ⟨1^{st} (e), O (F) (2^{nd} (e))⟩)$
34	33	a1d	$⊢ \neg T \in V \to ((F : A ⟶ R \land A \subseteq V) \to S (F) = (e \in E ⟼ ⟨1^{st} (e), O (F) (2^{nd} (e))⟩))$
35	23 34	pm2.61i	$⊢ (F : A ⟶ R \land A \subseteq V) \to S (F) = (e \in E ⟼ ⟨1^{st} (e), O (F) (2^{nd} (e))⟩)$

Metamath Proof Explorer

Theorem msubfval

Proof