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 ⊢ C = mCN ⁡ T
mrexval.v ⊢ V = mVR ⁡ T
mrexval.r ⊢ R = mREx ⁡ T
Assertion mrexval ⊢ T ∈ W → R = Word C ∪ 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 ∈ W → T ∈ 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 ∪ mVR ⁡ t = C ∪ V
10 wrdeq ⊢ mCN ⁡ t ∪ mVR ⁡ t = C ∪ V → Word mCN ⁡ t ∪ mVR ⁡ t = Word C ∪ V
11 9 10 syl ⊢ t = T → Word mCN ⁡ t ∪ mVR ⁡ t = Word C ∪ V
12 df-mrex ⊢ mREx = t ∈ V ⟼ Word mCN ⁡ t ∪ mVR ⁡ t
13 fvex ⊢ mCN ⁡ t ∈ V
14 fvex ⊢ mVR ⁡ t ∈ V
15 13 14 unex ⊢ mCN ⁡ t ∪ mVR ⁡ t ∈ V
16 15 wrdexi ⊢ Word mCN ⁡ t ∪ mVR ⁡ t ∈ V
17 11 12 16 fvmpt3i ⊢ T ∈ V → mREx ⁡ T = Word C ∪ V
18 4 17 syl ⊢ T ∈ W → mREx ⁡ T = Word C ∪ V
19 3 18 syl5eq ⊢ T ∈ W → R = Word C ∪ V