Theorem mvrsval

Description: The set of variables in an expression. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mvrsval.v	$$⊢V=\mathrm{mVR}\left(T\right)$$
	mvrsval.e	$$⊢E=\mathrm{mEx}\left(T\right)$$
	mvrsval.w	$$⊢W=\mathrm{mVars}\left(T\right)$$
Assertion	mvrsval	$$⊢X\in E\to W\left(X\right)=\mathrm{ran}{2}^{nd}\left(X\right)\cap V$$

Proof

Step	Hyp	Ref	Expression
1		mvrsval.v	$$⊢V=\mathrm{mVR}\left(T\right)$$
2		mvrsval.e	$$⊢E=\mathrm{mEx}\left(T\right)$$
3		mvrsval.w	$$⊢W=\mathrm{mVars}\left(T\right)$$
4		elfvex	$$⊢X\in \mathrm{mEx}\left(T\right)\to T\in \mathrm{V}$$
5	4 2	eleq2s	$$⊢X\in E\to T\in \mathrm{V}$$
6		fveq2	$$⊢t=T\to \mathrm{mEx}\left(t\right)=\mathrm{mEx}\left(T\right)$$
7	6 2	eqtr4di	$$⊢t=T\to \mathrm{mEx}\left(t\right)=E$$
8		fveq2	$$⊢t=T\to \mathrm{mVR}\left(t\right)=\mathrm{mVR}\left(T\right)$$
9	8 1	eqtr4di	$$⊢t=T\to \mathrm{mVR}\left(t\right)=V$$
10	9	ineq2d	$$⊢t=T\to \mathrm{ran}{2}^{nd}\left(e\right)\cap \mathrm{mVR}\left(t\right)=\mathrm{ran}{2}^{nd}\left(e\right)\cap V$$
11	7 10	mpteq12dv	$$⊢t=T\to \left(e\in \mathrm{mEx}\left(t\right)⟼\mathrm{ran}{2}^{nd}\left(e\right)\cap \mathrm{mVR}\left(t\right)\right)=\left(e\in E⟼\mathrm{ran}{2}^{nd}\left(e\right)\cap V\right)$$
12		df-mvrs	$$⊢\mathrm{mVars}=\left(t\in \mathrm{V}⟼\left(e\in \mathrm{mEx}\left(t\right)⟼\mathrm{ran}{2}^{nd}\left(e\right)\cap \mathrm{mVR}\left(t\right)\right)\right)$$
13	11 12 2	mptfvmpt	$$⊢T\in \mathrm{V}\to \mathrm{mVars}\left(T\right)=\left(e\in E⟼\mathrm{ran}{2}^{nd}\left(e\right)\cap V\right)$$
14	5 13	syl	$$⊢X\in E\to \mathrm{mVars}\left(T\right)=\left(e\in E⟼\mathrm{ran}{2}^{nd}\left(e\right)\cap V\right)$$
15	3 14	eqtrid	$$⊢X\in E\to W=\left(e\in E⟼\mathrm{ran}{2}^{nd}\left(e\right)\cap V\right)$$
16		fveq2	$$⊢e=X\to 2^{nd}\left(e\right)=2^{nd}\left(X\right)$$
17	16	rneqd	$$⊢e=X\to \mathrm{ran}{2}^{nd}\left(e\right)=\mathrm{ran}{2}^{nd}\left(X\right)$$
18	17	ineq1d	$$⊢e=X\to \mathrm{ran}{2}^{nd}\left(e\right)\cap V=\mathrm{ran}{2}^{nd}\left(X\right)\cap V$$
19	18	adantl	$$⊢\left(X\in E\wedge e=X\right)\to \mathrm{ran}{2}^{nd}\left(e\right)\cap V=\mathrm{ran}{2}^{nd}\left(X\right)\cap V$$
20		id	$$⊢X\in E\to X\in E$$
21		fvex	$$⊢2^{nd}\left(X\right)\in \mathrm{V}$$
22	21	rnex	$$⊢\mathrm{ran}{2}^{nd}\left(X\right)\in \mathrm{V}$$
23	22	inex1	$$⊢\mathrm{ran}{2}^{nd}\left(X\right)\cap V\in \mathrm{V}$$
24	23	a1i	$$⊢X\in E\to \mathrm{ran}{2}^{nd}\left(X\right)\cap V\in \mathrm{V}$$
25	15 19 20 24	fvmptd	$$⊢X\in E\to W\left(X\right)=\mathrm{ran}{2}^{nd}\left(X\right)\cap V$$