Theorem mrexval

Description: The set of "raw expressions", which are expressions without a typecode, that is, just sequences of constants and variables. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mrexval.c	|- C = ( mCN ` T )
	mrexval.v	|- V = ( mVR ` T )
	mrexval.r	|- R = ( mREx ` T )
Assertion	mrexval	|- ( T e. W -> R = Word ( C u. V ) )

Proof

Step	Hyp	Ref	Expression
1		mrexval.c	|- C = ( mCN ` T )
2		mrexval.v	|- V = ( mVR ` T )
3		mrexval.r	|- R = ( mREx ` T )
4		elex	|- ( T e. W -> T e. _V )
5		fveq2	|- ( t = T -> ( mCN ` t ) = ( mCN ` T ) )
6	5 1	eqtr4di	|- ( t = T -> ( mCN ` t ) = C )
7		fveq2	|- ( t = T -> ( mVR ` t ) = ( mVR ` T ) )
8	7 2	eqtr4di	|- ( t = T -> ( mVR ` t ) = V )
9	6 8	uneq12d	|- ( t = T -> ( ( mCN ` t ) u. ( mVR ` t ) ) = ( C u. V ) )
10		wrdeq	|- ( ( ( mCN ` t ) u. ( mVR ` t ) ) = ( C u. V ) -> Word ( ( mCN ` t ) u. ( mVR ` t ) ) = Word ( C u. V ) )
11	9 10	syl	|- ( t = T -> Word ( ( mCN ` t ) u. ( mVR ` t ) ) = Word ( C u. V ) )
12		df-mrex	|- mREx = ( t e. _V |-> Word ( ( mCN ` t ) u. ( mVR ` t ) ) )
13		fvex	|- ( mCN ` t ) e. _V
14		fvex	|- ( mVR ` t ) e. _V
15	13 14	unex	|- ( ( mCN ` t ) u. ( mVR ` t ) ) e. _V
16	15	wrdexi	|- Word ( ( mCN ` t ) u. ( mVR ` t ) ) e. _V
17	11 12 16	fvmpt3i	|- ( T e. _V -> ( mREx ` T ) = Word ( C u. V ) )
18	4 17	syl	|- ( T e. W -> ( mREx ` T ) = Word ( C u. V ) )
19	3 18	syl5eq	|- ( T e. W -> R = Word ( C u. V ) )