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. E -> ( W ` X ) = ( ran ( 2nd ` X ) i^i 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 e. ( mEx ` T ) -> T e. _V )
5	4 2	eleq2s	|- ( X e. E -> T e. _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 ( 2nd ` e ) i^i ( mVR ` t ) ) = ( ran ( 2nd ` e ) i^i V ) )
11	7 10	mpteq12dv	|- ( t = T -> ( e e. ( mEx ` t ) |-> ( ran ( 2nd ` e ) i^i ( mVR ` t ) ) ) = ( e e. E |-> ( ran ( 2nd ` e ) i^i V ) ) )
12		df-mvrs	|- mVars = ( t e. _V |-> ( e e. ( mEx ` t ) |-> ( ran ( 2nd ` e ) i^i ( mVR ` t ) ) ) )
13	11 12 2	mptfvmpt	|- ( T e. _V -> ( mVars ` T ) = ( e e. E |-> ( ran ( 2nd ` e ) i^i V ) ) )
14	5 13	syl	|- ( X e. E -> ( mVars ` T ) = ( e e. E |-> ( ran ( 2nd ` e ) i^i V ) ) )
15	3 14	syl5eq	|- ( X e. E -> W = ( e e. E |-> ( ran ( 2nd ` e ) i^i V ) ) )
16		fveq2	|- ( e = X -> ( 2nd ` e ) = ( 2nd ` X ) )
17	16	rneqd	|- ( e = X -> ran ( 2nd ` e ) = ran ( 2nd ` X ) )
18	17	ineq1d	|- ( e = X -> ( ran ( 2nd ` e ) i^i V ) = ( ran ( 2nd ` X ) i^i V ) )
19	18	adantl	|- ( ( X e. E /\ e = X ) -> ( ran ( 2nd ` e ) i^i V ) = ( ran ( 2nd ` X ) i^i V ) )
20		id	|- ( X e. E -> X e. E )
21		fvex	|- ( 2nd ` X ) e. _V
22	21	rnex	|- ran ( 2nd ` X ) e. _V
23	22	inex1	|- ( ran ( 2nd ` X ) i^i V ) e. _V
24	23	a1i	|- ( X e. E -> ( ran ( 2nd ` X ) i^i V ) e. _V )
25	15 19 20 24	fvmptd	|- ( X e. E -> ( W ` X ) = ( ran ( 2nd ` X ) i^i V ) )