Theorem mexval

Description: The set of expressions, which are pairs whose first element is a typecode, and whose second element is a raw expression. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mexval.k	$$⊢K=\mathrm{mTC}\left(T\right)$$
	mexval.e	$$⊢E=\mathrm{mEx}\left(T\right)$$
	mexval.r	$$⊢R=\mathrm{mREx}\left(T\right)$$
Assertion	mexval	$$⊢E=K\times R$$

Proof

Step	Hyp	Ref	Expression
1		mexval.k	$$⊢K=\mathrm{mTC}\left(T\right)$$
2		mexval.e	$$⊢E=\mathrm{mEx}\left(T\right)$$
3		mexval.r	$$⊢R=\mathrm{mREx}\left(T\right)$$
4		fveq2	$$⊢t=T\to \mathrm{mTC}\left(t\right)=\mathrm{mTC}\left(T\right)$$
5	4 1	eqtr4di	$$⊢t=T\to \mathrm{mTC}\left(t\right)=K$$
6		fveq2	$$⊢t=T\to \mathrm{mREx}\left(t\right)=\mathrm{mREx}\left(T\right)$$
7	6 3	eqtr4di	$$⊢t=T\to \mathrm{mREx}\left(t\right)=R$$
8	5 7	xpeq12d	$$⊢t=T\to \mathrm{mTC}\left(t\right)\times \mathrm{mREx}\left(t\right)=K\times R$$
9		df-mex	$$⊢\mathrm{mEx}=\left(t\in \mathrm{V}⟼\mathrm{mTC}\left(t\right)\times \mathrm{mREx}\left(t\right)\right)$$
10		fvex	$$⊢\mathrm{mTC}\left(t\right)\in \mathrm{V}$$
11		fvex	$$⊢\mathrm{mREx}\left(t\right)\in \mathrm{V}$$
12	10 11	xpex	$$⊢\mathrm{mTC}\left(t\right)\times \mathrm{mREx}\left(t\right)\in \mathrm{V}$$
13	8 9 12	fvmpt3i	$$⊢T\in \mathrm{V}\to \mathrm{mEx}\left(T\right)=K\times R$$
14		xp0	$$⊢K\times \varnothing =\varnothing$$
15	14	eqcomi	$$⊢\varnothing =K\times \varnothing$$
16		fvprc	$$⊢\neg T\in \mathrm{V}\to \mathrm{mEx}\left(T\right)=\varnothing$$
17		fvprc	$$⊢\neg T\in \mathrm{V}\to \mathrm{mREx}\left(T\right)=\varnothing$$
18	3 17	syl5eq	$$⊢\neg T\in \mathrm{V}\to R=\varnothing$$
19	18	xpeq2d	$$⊢\neg T\in \mathrm{V}\to K\times R=K\times \varnothing$$
20	15 16 19	3eqtr4a	$$⊢\neg T\in \mathrm{V}\to \mathrm{mEx}\left(T\right)=K\times R$$
21	13 20	pm2.61i	$$⊢\mathrm{mEx}\left(T\right)=K\times R$$
22	2 21	eqtri	$$⊢E=K\times R$$