Theorem mexval2

Description: The set of expressions, which are pairs whose first element is a typecode, and whose second element is a list of constants and variables. (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)$$
	mexval2.c	$$⊢C=\mathrm{mCN}\left(T\right)$$
	mexval2.v	$$⊢V=\mathrm{mVR}\left(T\right)$$
Assertion	mexval2	$$⊢E=K\times \mathrm{Word}\left(C\cup V\right)$$

Proof

Step	Hyp	Ref	Expression
1		mexval.k	$$⊢K=\mathrm{mTC}\left(T\right)$$
2		mexval.e	$$⊢E=\mathrm{mEx}\left(T\right)$$
3		mexval2.c	$$⊢C=\mathrm{mCN}\left(T\right)$$
4		mexval2.v	$$⊢V=\mathrm{mVR}\left(T\right)$$
5		eqid	$$⊢\mathrm{mREx}\left(T\right)=\mathrm{mREx}\left(T\right)$$
6	1 2 5	mexval	$$⊢E=K\times \mathrm{mREx}\left(T\right)$$
7	3 4 5	mrexval	$$⊢T\in \mathrm{V}\to \mathrm{mREx}\left(T\right)=\mathrm{Word}\left(C\cup V\right)$$
8	7	xpeq2d	$$⊢T\in \mathrm{V}\to K\times \mathrm{mREx}\left(T\right)=K\times \mathrm{Word}\left(C\cup V\right)$$
9	6 8	syl5eq	$$⊢T\in \mathrm{V}\to E=K\times \mathrm{Word}\left(C\cup V\right)$$
10		0xp	$$⊢\varnothing \times \mathrm{Word}\left(C\cup V\right)=\varnothing$$
11	10	eqcomi	$$⊢\varnothing =\varnothing \times \mathrm{Word}\left(C\cup V\right)$$
12		fvprc	$$⊢\neg T\in \mathrm{V}\to \mathrm{mEx}\left(T\right)=\varnothing$$
13	2 12	syl5eq	$$⊢\neg T\in \mathrm{V}\to E=\varnothing$$
14		fvprc	$$⊢\neg T\in \mathrm{V}\to \mathrm{mTC}\left(T\right)=\varnothing$$
15	1 14	syl5eq	$$⊢\neg T\in \mathrm{V}\to K=\varnothing$$
16	15	xpeq1d	$$⊢\neg T\in \mathrm{V}\to K\times \mathrm{Word}\left(C\cup V\right)=\varnothing \times \mathrm{Word}\left(C\cup V\right)$$
17	11 13 16	3eqtr4a	$$⊢\neg T\in \mathrm{V}\to E=K\times \mathrm{Word}\left(C\cup V\right)$$
18	9 17	pm2.61i	$$⊢E=K\times \mathrm{Word}\left(C\cup V\right)$$