Theorem mvrsval

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

	Ref	Expression
Hypotheses	mvrsval.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
	mvrsval.e	⊢ 𝐸 = ( mEx ‘ 𝑇 )
	mvrsval.w	⊢ 𝑊 = ( mVars ‘ 𝑇 )
Assertion	mvrsval	⊢ ( 𝑋 ∈ 𝐸 → ( 𝑊 ‘ 𝑋 ) = ( ran ( 2nd ‘ 𝑋 ) ∩ 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		mvrsval.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
2		mvrsval.e	⊢ 𝐸 = ( mEx ‘ 𝑇 )
3		mvrsval.w	⊢ 𝑊 = ( mVars ‘ 𝑇 )
4		elfvex	⊢ ( 𝑋 ∈ ( mEx ‘ 𝑇 ) → 𝑇 ∈ V )
5	4 2	eleq2s	⊢ ( 𝑋 ∈ 𝐸 → 𝑇 ∈ V )
6		fveq2	⊢ ( 𝑡 = 𝑇 → ( mEx ‘ 𝑡 ) = ( mEx ‘ 𝑇 ) )
7	6 2	eqtr4di	⊢ ( 𝑡 = 𝑇 → ( mEx ‘ 𝑡 ) = 𝐸 )
8		fveq2	⊢ ( 𝑡 = 𝑇 → ( mVR ‘ 𝑡 ) = ( mVR ‘ 𝑇 ) )
9	8 1	eqtr4di	⊢ ( 𝑡 = 𝑇 → ( mVR ‘ 𝑡 ) = 𝑉 )
10	9	ineq2d	⊢ ( 𝑡 = 𝑇 → ( ran ( 2nd ‘ 𝑒 ) ∩ ( mVR ‘ 𝑡 ) ) = ( ran ( 2nd ‘ 𝑒 ) ∩ 𝑉 ) )
11	7 10	mpteq12dv	⊢ ( 𝑡 = 𝑇 → ( 𝑒 ∈ ( mEx ‘ 𝑡 ) ↦ ( ran ( 2nd ‘ 𝑒 ) ∩ ( mVR ‘ 𝑡 ) ) ) = ( 𝑒 ∈ 𝐸 ↦ ( ran ( 2nd ‘ 𝑒 ) ∩ 𝑉 ) ) )
12		df-mvrs	⊢ mVars = ( 𝑡 ∈ V ↦ ( 𝑒 ∈ ( mEx ‘ 𝑡 ) ↦ ( ran ( 2nd ‘ 𝑒 ) ∩ ( mVR ‘ 𝑡 ) ) ) )
13	11 12 2	mptfvmpt	⊢ ( 𝑇 ∈ V → ( mVars ‘ 𝑇 ) = ( 𝑒 ∈ 𝐸 ↦ ( ran ( 2nd ‘ 𝑒 ) ∩ 𝑉 ) ) )
14	5 13	syl	⊢ ( 𝑋 ∈ 𝐸 → ( mVars ‘ 𝑇 ) = ( 𝑒 ∈ 𝐸 ↦ ( ran ( 2nd ‘ 𝑒 ) ∩ 𝑉 ) ) )
15	3 14	syl5eq	⊢ ( 𝑋 ∈ 𝐸 → 𝑊 = ( 𝑒 ∈ 𝐸 ↦ ( ran ( 2nd ‘ 𝑒 ) ∩ 𝑉 ) ) )
16		fveq2	⊢ ( 𝑒 = 𝑋 → ( 2nd ‘ 𝑒 ) = ( 2nd ‘ 𝑋 ) )
17	16	rneqd	⊢ ( 𝑒 = 𝑋 → ran ( 2nd ‘ 𝑒 ) = ran ( 2nd ‘ 𝑋 ) )
18	17	ineq1d	⊢ ( 𝑒 = 𝑋 → ( ran ( 2nd ‘ 𝑒 ) ∩ 𝑉 ) = ( ran ( 2nd ‘ 𝑋 ) ∩ 𝑉 ) )
19	18	adantl	⊢ ( ( 𝑋 ∈ 𝐸 ∧ 𝑒 = 𝑋 ) → ( ran ( 2nd ‘ 𝑒 ) ∩ 𝑉 ) = ( ran ( 2nd ‘ 𝑋 ) ∩ 𝑉 ) )
20		id	⊢ ( 𝑋 ∈ 𝐸 → 𝑋 ∈ 𝐸 )
21		fvex	⊢ ( 2nd ‘ 𝑋 ) ∈ V
22	21	rnex	⊢ ran ( 2nd ‘ 𝑋 ) ∈ V
23	22	inex1	⊢ ( ran ( 2nd ‘ 𝑋 ) ∩ 𝑉 ) ∈ V
24	23	a1i	⊢ ( 𝑋 ∈ 𝐸 → ( ran ( 2nd ‘ 𝑋 ) ∩ 𝑉 ) ∈ V )
25	15 19 20 24	fvmptd	⊢ ( 𝑋 ∈ 𝐸 → ( 𝑊 ‘ 𝑋 ) = ( ran ( 2nd ‘ 𝑋 ) ∩ 𝑉 ) )