# Metamath Proof Explorer

## 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 ( 𝐶𝑉 ) )