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	⊢ 𝐶 = ( mCN ‘ 𝑇 )
	mrexval.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
	mrexval.r	⊢ 𝑅 = ( mREx ‘ 𝑇 )
Assertion	mrexval	⊢ ( 𝑇 ∈ 𝑊 → 𝑅 = Word ( 𝐶 ∪ 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		mrexval.c	⊢ 𝐶 = ( mCN ‘ 𝑇 )
2		mrexval.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
3		mrexval.r	⊢ 𝑅 = ( mREx ‘ 𝑇 )
4		elex	⊢ ( 𝑇 ∈ 𝑊 → 𝑇 ∈ V )
5		fveq2	⊢ ( 𝑡 = 𝑇 → ( mCN ‘ 𝑡 ) = ( mCN ‘ 𝑇 ) )
6	5 1	eqtr4di	⊢ ( 𝑡 = 𝑇 → ( mCN ‘ 𝑡 ) = 𝐶 )
7		fveq2	⊢ ( 𝑡 = 𝑇 → ( mVR ‘ 𝑡 ) = ( mVR ‘ 𝑇 ) )
8	7 2	eqtr4di	⊢ ( 𝑡 = 𝑇 → ( mVR ‘ 𝑡 ) = 𝑉 )
9	6 8	uneq12d	⊢ ( 𝑡 = 𝑇 → ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) = ( 𝐶 ∪ 𝑉 ) )
10		wrdeq	⊢ ( ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) = ( 𝐶 ∪ 𝑉 ) → Word ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) = Word ( 𝐶 ∪ 𝑉 ) )
11	9 10	syl	⊢ ( 𝑡 = 𝑇 → Word ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) = Word ( 𝐶 ∪ 𝑉 ) )
12		df-mrex	⊢ mREx = ( 𝑡 ∈ V ↦ Word ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) )
13		fvex	⊢ ( mCN ‘ 𝑡 ) ∈ V
14		fvex	⊢ ( mVR ‘ 𝑡 ) ∈ V
15	13 14	unex	⊢ ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) ∈ V
16	15	wrdexi	⊢ Word ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) ∈ V
17	11 12 16	fvmpt3i	⊢ ( 𝑇 ∈ V → ( mREx ‘ 𝑇 ) = Word ( 𝐶 ∪ 𝑉 ) )
18	4 17	syl	⊢ ( 𝑇 ∈ 𝑊 → ( mREx ‘ 𝑇 ) = Word ( 𝐶 ∪ 𝑉 ) )
19	3 18	syl5eq	⊢ ( 𝑇 ∈ 𝑊 → 𝑅 = Word ( 𝐶 ∪ 𝑉 ) )