Theorem mvtval

Description: The set of variable typecodes. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mvtval.f	$$⊢V=\mathrm{mVT}\left(T\right)$$
	mvtval.y	$$⊢Y=\mathrm{mType}\left(T\right)$$
Assertion	mvtval	$$⊢V=\mathrm{ran}Y$$

Proof

Step	Hyp	Ref	Expression
1		mvtval.f	$$⊢V=\mathrm{mVT}\left(T\right)$$
2		mvtval.y	$$⊢Y=\mathrm{mType}\left(T\right)$$
3		fveq2	$$⊢t=T\to \mathrm{mType}\left(t\right)=\mathrm{mType}\left(T\right)$$
4	3	rneqd	$$⊢t=T\to \mathrm{ran}\mathrm{mType}\left(t\right)=\mathrm{ran}\mathrm{mType}\left(T\right)$$
5		df-mvt	$$⊢\mathrm{mVT}=\left(t\in \mathrm{V}⟼\mathrm{ran}\mathrm{mType}\left(t\right)\right)$$
6		fvex	$$⊢\mathrm{mType}\left(T\right)\in \mathrm{V}$$
7	6	rnex	$$⊢\mathrm{ran}\mathrm{mType}\left(T\right)\in \mathrm{V}$$
8	4 5 7	fvmpt	$$⊢T\in \mathrm{V}\to \mathrm{mVT}\left(T\right)=\mathrm{ran}\mathrm{mType}\left(T\right)$$
9		rn0	$$⊢\mathrm{ran}\varnothing =\varnothing$$
10	9	eqcomi	$$⊢\varnothing =\mathrm{ran}\varnothing$$
11		fvprc	$$⊢\neg T\in \mathrm{V}\to \mathrm{mVT}\left(T\right)=\varnothing$$
12		fvprc	$$⊢\neg T\in \mathrm{V}\to \mathrm{mType}\left(T\right)=\varnothing$$
13	12	rneqd	$$⊢\neg T\in \mathrm{V}\to \mathrm{ran}\mathrm{mType}\left(T\right)=\mathrm{ran}\varnothing$$
14	10 11 13	3eqtr4a	$$⊢\neg T\in \mathrm{V}\to \mathrm{mVT}\left(T\right)=\mathrm{ran}\mathrm{mType}\left(T\right)$$
15	8 14	pm2.61i	$$⊢\mathrm{mVT}\left(T\right)=\mathrm{ran}\mathrm{mType}\left(T\right)$$
16	2	rneqi	$$⊢\mathrm{ran}Y=\mathrm{ran}\mathrm{mType}\left(T\right)$$
17	15 1 16	3eqtr4i	$$⊢V=\mathrm{ran}Y$$