Metamath Proof Explorer

Theorem mvrsval

Description: The set of variables in an expression. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mvrsval.v ⊢ V = mVR ⁡ T
mvrsval.e ⊢ E = mEx ⁡ T
mvrsval.w ⊢ W = mVars ⁡ T
Assertion mvrsval ⊢ X ∈ E → W ⁡ X = ran ⁡ 2 nd ⁡ X ∩ V

Proof

Step Hyp Ref Expression
1 mvrsval.v ⊢ V = mVR ⁡ T
2 mvrsval.e ⊢ E = mEx ⁡ T
3 mvrsval.w ⊢ W = mVars ⁡ T
4 elfvex ⊢ X ∈ mEx ⁡ T → T ∈ V
5 4 2 eleq2s ⊢ X ∈ E → T ∈ V
6 fveq2 ⊢ t = T → mEx ⁡ t = mEx ⁡ T
7 6 2 eqtr4di ⊢ t = T → mEx ⁡ t = E
8 fveq2 ⊢ t = T → mVR ⁡ t = mVR ⁡ T
9 8 1 eqtr4di ⊢ t = T → mVR ⁡ t = V
10 9 ineq2d ⊢ t = T → ran ⁡ 2 nd ⁡ e ∩ mVR ⁡ t = ran ⁡ 2 nd ⁡ e ∩ V
11 7 10 mpteq12dv ⊢ t = T → e ∈ mEx ⁡ t ⟼ ran ⁡ 2 nd ⁡ e ∩ mVR ⁡ t = e ∈ E ⟼ ran ⁡ 2 nd ⁡ e ∩ V
12 df-mvrs ⊢ mVars = t ∈ V ⟼ e ∈ mEx ⁡ t ⟼ ran ⁡ 2 nd ⁡ e ∩ mVR ⁡ t
13 11 12 2 mptfvmpt ⊢ T ∈ V → mVars ⁡ T = e ∈ E ⟼ ran ⁡ 2 nd ⁡ e ∩ V
14 5 13 syl ⊢ X ∈ E → mVars ⁡ T = e ∈ E ⟼ ran ⁡ 2 nd ⁡ e ∩ V
15 3 14 syl5eq ⊢ X ∈ E → W = e ∈ E ⟼ ran ⁡ 2 nd ⁡ e ∩ V
16 fveq2 ⊢ e = X → 2 nd ⁡ e = 2 nd ⁡ X
17 16 rneqd ⊢ e = X → ran ⁡ 2 nd ⁡ e = ran ⁡ 2 nd ⁡ X
18 17 ineq1d ⊢ e = X → ran ⁡ 2 nd ⁡ e ∩ V = ran ⁡ 2 nd ⁡ X ∩ V
19 18 adantl ⊢ X ∈ E ∧ e = X → ran ⁡ 2 nd ⁡ e ∩ V = ran ⁡ 2 nd ⁡ X ∩ V
20 id ⊢ X ∈ E → X ∈ E
21 fvex ⊢ 2 nd ⁡ X ∈ V
22 21 rnex ⊢ ran ⁡ 2 nd ⁡ X ∈ V
23 22 inex1 ⊢ ran ⁡ 2 nd ⁡ X ∩ V ∈ V
24 23 a1i ⊢ X ∈ E → ran ⁡ 2 nd ⁡ X ∩ V ∈ V
25 15 19 20 24 fvmptd ⊢ X ∈ E → W ⁡ X = ran ⁡ 2 nd ⁡ X ∩ V