Metamath Proof Explorer

Theorem msubvrs

Description: The set of variables in a substitution is the union, indexed by the variables in the original expression, of the variables in the substitution to that variable. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses msubvrs.s 
|- S = ( mSubst ` T )
msubvrs.e 
|- E = ( mEx ` T )
msubvrs.v 
|- V = ( mVars ` T )
msubvrs.h 
|- H = ( mVH ` T )
Assertion msubvrs 
|- ( ( T e. mFS /\ F e. ran S /\ X e. E ) -> ( V ` ( F ` X ) ) = U_ x e. ( V ` X ) ( V ` ( F ` ( H ` x ) ) ) )

Proof

Step Hyp Ref Expression
1 msubvrs.s 
 |-  S = ( mSubst ` T )
2 msubvrs.e 
 |-  E = ( mEx ` T )
3 msubvrs.v 
 |-  V = ( mVars ` T )
4 msubvrs.h 
 |-  H = ( mVH ` T )
5 eqid 
 |-  ( mRSubst ` T ) = ( mRSubst ` T )
6 2 5 1 elmsubrn 
 |-  ran S = ran ( f e. ran ( mRSubst ` T ) |-> ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) )
7 6 eleq2i 
 |-  ( F e. ran S <-> F e. ran ( f e. ran ( mRSubst ` T ) |-> ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ) )
8 eqid 
 |-  ( f e. ran ( mRSubst ` T ) |-> ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ) = ( f e. ran ( mRSubst ` T ) |-> ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) )
9 2 fvexi 
 |-  E e. _V
10 9 mptex 
 |-  ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) e. _V
11 8 10 elrnmpti 
 |-  ( F e. ran ( f e. ran ( mRSubst ` T ) |-> ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ) <-> E. f e. ran ( mRSubst ` T ) F = ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) )
12 7 11 bitri 
 |-  ( F e. ran S <-> E. f e. ran ( mRSubst ` T ) F = ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) )
13 simp2 
 |-  ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) -> f e. ran ( mRSubst ` T ) )
14 simp3 
 |-  ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) -> X e. E )
15 eqid 
 |-  ( mTC ` T ) = ( mTC ` T )
16 eqid 
 |-  ( mREx ` T ) = ( mREx ` T )
17 15 2 16 mexval 
 |-  E = ( ( mTC ` T ) X. ( mREx ` T ) )
18 14 17 eleqtrdi 
 |-  ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) -> X e. ( ( mTC ` T ) X. ( mREx ` T ) ) )
19 xp2nd 
 |-  ( X e. ( ( mTC ` T ) X. ( mREx ` T ) ) -> ( 2nd ` X ) e. ( mREx ` T ) )
20 18 19 syl 
 |-  ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) -> ( 2nd ` X ) e. ( mREx ` T ) )
21 eqid 
 |-  ( mVR ` T ) = ( mVR ` T )
22 5 21 16 mrsubvrs 
 |-  ( ( f e. ran ( mRSubst ` T ) /\ ( 2nd ` X ) e. ( mREx ` T ) ) -> ( ran ( f ` ( 2nd ` X ) ) i^i ( mVR ` T ) ) = U_ x e. ( ran ( 2nd ` X ) i^i ( mVR ` T ) ) ( ran ( f ` <" x "> ) i^i ( mVR ` T ) ) )
23 13 20 22 syl2anc 
 |-  ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) -> ( ran ( f ` ( 2nd ` X ) ) i^i ( mVR ` T ) ) = U_ x e. ( ran ( 2nd ` X ) i^i ( mVR ` T ) ) ( ran ( f ` <" x "> ) i^i ( mVR ` T ) ) )
24 fveq2 
 |-  ( e = X -> ( 1st ` e ) = ( 1st ` X ) )
25 2fveq3 
 |-  ( e = X -> ( f ` ( 2nd ` e ) ) = ( f ` ( 2nd ` X ) ) )
26 24 25 opeq12d 
 |-  ( e = X -> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. = <. ( 1st ` X ) , ( f ` ( 2nd ` X ) ) >. )
27 eqid 
 |-  ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) = ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. )
28 opex 
 |-  <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. e. _V
29 26 27 28 fvmpt3i 
 |-  ( X e. E -> ( ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ` X ) = <. ( 1st ` X ) , ( f ` ( 2nd ` X ) ) >. )
30 14 29 syl 
 |-  ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) -> ( ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ` X ) = <. ( 1st ` X ) , ( f ` ( 2nd ` X ) ) >. )
31 30 fveq2d 
 |-  ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) -> ( V ` ( ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ` X ) ) = ( V ` <. ( 1st ` X ) , ( f ` ( 2nd ` X ) ) >. ) )
32 xp1st 
 |-  ( X e. ( ( mTC ` T ) X. ( mREx ` T ) ) -> ( 1st ` X ) e. ( mTC ` T ) )
33 18 32 syl 
 |-  ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) -> ( 1st ` X ) e. ( mTC ` T ) )
34 5 16 mrsubf 
 |-  ( f e. ran ( mRSubst ` T ) -> f : ( mREx ` T ) --> ( mREx ` T ) )
35 13 34 syl 
 |-  ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) -> f : ( mREx ` T ) --> ( mREx ` T ) )
36 19 17 eleq2s 
 |-  ( X e. E -> ( 2nd ` X ) e. ( mREx ` T ) )
37 14 36 syl 
 |-  ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) -> ( 2nd ` X ) e. ( mREx ` T ) )
38 35 37 ffvelrnd 
 |-  ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) -> ( f ` ( 2nd ` X ) ) e. ( mREx ` T ) )
39 opelxpi 
 |-  ( ( ( 1st ` X ) e. ( mTC ` T ) /\ ( f ` ( 2nd ` X ) ) e. ( mREx ` T ) ) -> <. ( 1st ` X ) , ( f ` ( 2nd ` X ) ) >. e. ( ( mTC ` T ) X. ( mREx ` T ) ) )
40 33 38 39 syl2anc 
 |-  ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) -> <. ( 1st ` X ) , ( f ` ( 2nd ` X ) ) >. e. ( ( mTC ` T ) X. ( mREx ` T ) ) )
41 40 17 eleqtrrdi 
 |-  ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) -> <. ( 1st ` X ) , ( f ` ( 2nd ` X ) ) >. e. E )
42 21 2 3 mvrsval 
 |-  ( <. ( 1st ` X ) , ( f ` ( 2nd ` X ) ) >. e. E -> ( V ` <. ( 1st ` X ) , ( f ` ( 2nd ` X ) ) >. ) = ( ran ( 2nd ` <. ( 1st ` X ) , ( f ` ( 2nd ` X ) ) >. ) i^i ( mVR ` T ) ) )
43 41 42 syl 
 |-  ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) -> ( V ` <. ( 1st ` X ) , ( f ` ( 2nd ` X ) ) >. ) = ( ran ( 2nd ` <. ( 1st ` X ) , ( f ` ( 2nd ` X ) ) >. ) i^i ( mVR ` T ) ) )
44 fvex 
 |-  ( 1st ` X ) e. _V
45 fvex 
 |-  ( f ` ( 2nd ` X ) ) e. _V
46 44 45 op2nd 
 |-  ( 2nd ` <. ( 1st ` X ) , ( f ` ( 2nd ` X ) ) >. ) = ( f ` ( 2nd ` X ) )
47 46 a1i 
 |-  ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) -> ( 2nd ` <. ( 1st ` X ) , ( f ` ( 2nd ` X ) ) >. ) = ( f ` ( 2nd ` X ) ) )
48 47 rneqd 
 |-  ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) -> ran ( 2nd ` <. ( 1st ` X ) , ( f ` ( 2nd ` X ) ) >. ) = ran ( f ` ( 2nd ` X ) ) )
49 48 ineq1d 
 |-  ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) -> ( ran ( 2nd ` <. ( 1st ` X ) , ( f ` ( 2nd ` X ) ) >. ) i^i ( mVR ` T ) ) = ( ran ( f ` ( 2nd ` X ) ) i^i ( mVR ` T ) ) )
50 31 43 49 3eqtrd 
 |-  ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) -> ( V ` ( ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ` X ) ) = ( ran ( f ` ( 2nd ` X ) ) i^i ( mVR ` T ) ) )
51 21 2 3 mvrsval 
 |-  ( X e. E -> ( V ` X ) = ( ran ( 2nd ` X ) i^i ( mVR ` T ) ) )
52 14 51 syl 
 |-  ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) -> ( V ` X ) = ( ran ( 2nd ` X ) i^i ( mVR ` T ) ) )
53 52 iuneq1d 
 |-  ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) -> U_ x e. ( V ` X ) ( V ` ( ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ` ( H ` x ) ) ) = U_ x e. ( ran ( 2nd ` X ) i^i ( mVR ` T ) ) ( V ` ( ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ` ( H ` x ) ) ) )
54 21 2 4 mvhf 
 |-  ( T e. mFS -> H : ( mVR ` T ) --> E )
55 54 3ad2ant1 
 |-  ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) -> H : ( mVR ` T ) --> E )
56 inss2 
 |-  ( ran ( 2nd ` X ) i^i ( mVR ` T ) ) C_ ( mVR ` T )
57 56 sseli 
 |-  ( x e. ( ran ( 2nd ` X ) i^i ( mVR ` T ) ) -> x e. ( mVR ` T ) )
58 ffvelrn 
 |-  ( ( H : ( mVR ` T ) --> E /\ x e. ( mVR ` T ) ) -> ( H ` x ) e. E )
59 55 57 58 syl2an 
 |-  ( ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) /\ x e. ( ran ( 2nd ` X ) i^i ( mVR ` T ) ) ) -> ( H ` x ) e. E )
60 fveq2 
 |-  ( e = ( H ` x ) -> ( 1st ` e ) = ( 1st ` ( H ` x ) ) )
61 2fveq3 
 |-  ( e = ( H ` x ) -> ( f ` ( 2nd ` e ) ) = ( f ` ( 2nd ` ( H ` x ) ) ) )
62 60 61 opeq12d 
 |-  ( e = ( H ` x ) -> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. = <. ( 1st ` ( H ` x ) ) , ( f ` ( 2nd ` ( H ` x ) ) ) >. )
63 62 27 28 fvmpt3i 
 |-  ( ( H ` x ) e. E -> ( ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ` ( H ` x ) ) = <. ( 1st ` ( H ` x ) ) , ( f ` ( 2nd ` ( H ` x ) ) ) >. )
64 59 63 syl 
 |-  ( ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) /\ x e. ( ran ( 2nd ` X ) i^i ( mVR ` T ) ) ) -> ( ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ` ( H ` x ) ) = <. ( 1st ` ( H ` x ) ) , ( f ` ( 2nd ` ( H ` x ) ) ) >. )
65 57 adantl 
 |-  ( ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) /\ x e. ( ran ( 2nd ` X ) i^i ( mVR ` T ) ) ) -> x e. ( mVR ` T ) )
66 eqid 
 |-  ( mType ` T ) = ( mType ` T )
67 21 66 4 mvhval 
 |-  ( x e. ( mVR ` T ) -> ( H ` x ) = <. ( ( mType ` T ) ` x ) , <" x "> >. )
68 65 67 syl 
 |-  ( ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) /\ x e. ( ran ( 2nd ` X ) i^i ( mVR ` T ) ) ) -> ( H ` x ) = <. ( ( mType ` T ) ` x ) , <" x "> >. )
69 fvex 
 |-  ( ( mType ` T ) ` x ) e. _V
70 s1cli 
 |-  <" x "> e. Word _V
71 70 elexi 
 |-  <" x "> e. _V
72 69 71 op1std 
 |-  ( ( H ` x ) = <. ( ( mType ` T ) ` x ) , <" x "> >. -> ( 1st ` ( H ` x ) ) = ( ( mType ` T ) ` x ) )
73 68 72 syl 
 |-  ( ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) /\ x e. ( ran ( 2nd ` X ) i^i ( mVR ` T ) ) ) -> ( 1st ` ( H ` x ) ) = ( ( mType ` T ) ` x ) )
74 69 71 op2ndd 
 |-  ( ( H ` x ) = <. ( ( mType ` T ) ` x ) , <" x "> >. -> ( 2nd ` ( H ` x ) ) = <" x "> )
75 68 74 syl 
 |-  ( ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) /\ x e. ( ran ( 2nd ` X ) i^i ( mVR ` T ) ) ) -> ( 2nd ` ( H ` x ) ) = <" x "> )
76 75 fveq2d 
 |-  ( ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) /\ x e. ( ran ( 2nd ` X ) i^i ( mVR ` T ) ) ) -> ( f ` ( 2nd ` ( H ` x ) ) ) = ( f ` <" x "> ) )
77 73 76 opeq12d 
 |-  ( ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) /\ x e. ( ran ( 2nd ` X ) i^i ( mVR ` T ) ) ) -> <. ( 1st ` ( H ` x ) ) , ( f ` ( 2nd ` ( H ` x ) ) ) >. = <. ( ( mType ` T ) ` x ) , ( f ` <" x "> ) >. )
78 64 77 eqtrd 
 |-  ( ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) /\ x e. ( ran ( 2nd ` X ) i^i ( mVR ` T ) ) ) -> ( ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ` ( H ` x ) ) = <. ( ( mType ` T ) ` x ) , ( f ` <" x "> ) >. )
79 78 fveq2d 
 |-  ( ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) /\ x e. ( ran ( 2nd ` X ) i^i ( mVR ` T ) ) ) -> ( V ` ( ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ` ( H ` x ) ) ) = ( V ` <. ( ( mType ` T ) ` x ) , ( f ` <" x "> ) >. ) )
80 simpl1 
 |-  ( ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) /\ x e. ( ran ( 2nd ` X ) i^i ( mVR ` T ) ) ) -> T e. mFS )
81 21 15 66 mtyf2 
 |-  ( T e. mFS -> ( mType ` T ) : ( mVR ` T ) --> ( mTC ` T ) )
82 80 81 syl 
 |-  ( ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) /\ x e. ( ran ( 2nd ` X ) i^i ( mVR ` T ) ) ) -> ( mType ` T ) : ( mVR ` T ) --> ( mTC ` T ) )
83 82 65 ffvelrnd 
 |-  ( ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) /\ x e. ( ran ( 2nd ` X ) i^i ( mVR ` T ) ) ) -> ( ( mType ` T ) ` x ) e. ( mTC ` T ) )
84 35 adantr 
 |-  ( ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) /\ x e. ( ran ( 2nd ` X ) i^i ( mVR ` T ) ) ) -> f : ( mREx ` T ) --> ( mREx ` T ) )
85 elun2 
 |-  ( x e. ( mVR ` T ) -> x e. ( ( mCN ` T ) u. ( mVR ` T ) ) )
86 65 85 syl 
 |-  ( ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) /\ x e. ( ran ( 2nd ` X ) i^i ( mVR ` T ) ) ) -> x e. ( ( mCN ` T ) u. ( mVR ` T ) ) )
87 86 s1cld 
 |-  ( ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) /\ x e. ( ran ( 2nd ` X ) i^i ( mVR ` T ) ) ) -> <" x "> e. Word ( ( mCN ` T ) u. ( mVR ` T ) ) )
88 eqid 
 |-  ( mCN ` T ) = ( mCN ` T )
89 88 21 16 mrexval 
 |-  ( T e. mFS -> ( mREx ` T ) = Word ( ( mCN ` T ) u. ( mVR ` T ) ) )
90 80 89 syl 
 |-  ( ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) /\ x e. ( ran ( 2nd ` X ) i^i ( mVR ` T ) ) ) -> ( mREx ` T ) = Word ( ( mCN ` T ) u. ( mVR ` T ) ) )
91 87 90 eleqtrrd 
 |-  ( ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) /\ x e. ( ran ( 2nd ` X ) i^i ( mVR ` T ) ) ) -> <" x "> e. ( mREx ` T ) )
92 84 91 ffvelrnd 
 |-  ( ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) /\ x e. ( ran ( 2nd ` X ) i^i ( mVR ` T ) ) ) -> ( f ` <" x "> ) e. ( mREx ` T ) )
93 opelxpi 
 |-  ( ( ( ( mType ` T ) ` x ) e. ( mTC ` T ) /\ ( f ` <" x "> ) e. ( mREx ` T ) ) -> <. ( ( mType ` T ) ` x ) , ( f ` <" x "> ) >. e. ( ( mTC ` T ) X. ( mREx ` T ) ) )
94 83 92 93 syl2anc 
 |-  ( ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) /\ x e. ( ran ( 2nd ` X ) i^i ( mVR ` T ) ) ) -> <. ( ( mType ` T ) ` x ) , ( f ` <" x "> ) >. e. ( ( mTC ` T ) X. ( mREx ` T ) ) )
95 94 17 eleqtrrdi 
 |-  ( ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) /\ x e. ( ran ( 2nd ` X ) i^i ( mVR ` T ) ) ) -> <. ( ( mType ` T ) ` x ) , ( f ` <" x "> ) >. e. E )
96 21 2 3 mvrsval 
 |-  ( <. ( ( mType ` T ) ` x ) , ( f ` <" x "> ) >. e. E -> ( V ` <. ( ( mType ` T ) ` x ) , ( f ` <" x "> ) >. ) = ( ran ( 2nd ` <. ( ( mType ` T ) ` x ) , ( f ` <" x "> ) >. ) i^i ( mVR ` T ) ) )
97 95 96 syl 
 |-  ( ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) /\ x e. ( ran ( 2nd ` X ) i^i ( mVR ` T ) ) ) -> ( V ` <. ( ( mType ` T ) ` x ) , ( f ` <" x "> ) >. ) = ( ran ( 2nd ` <. ( ( mType ` T ) ` x ) , ( f ` <" x "> ) >. ) i^i ( mVR ` T ) ) )
98 fvex 
 |-  ( f ` <" x "> ) e. _V
99 69 98 op2nd 
 |-  ( 2nd ` <. ( ( mType ` T ) ` x ) , ( f ` <" x "> ) >. ) = ( f ` <" x "> )
100 99 a1i 
 |-  ( ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) /\ x e. ( ran ( 2nd ` X ) i^i ( mVR ` T ) ) ) -> ( 2nd ` <. ( ( mType ` T ) ` x ) , ( f ` <" x "> ) >. ) = ( f ` <" x "> ) )
101 100 rneqd 
 |-  ( ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) /\ x e. ( ran ( 2nd ` X ) i^i ( mVR ` T ) ) ) -> ran ( 2nd ` <. ( ( mType ` T ) ` x ) , ( f ` <" x "> ) >. ) = ran ( f ` <" x "> ) )
102 101 ineq1d 
 |-  ( ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) /\ x e. ( ran ( 2nd ` X ) i^i ( mVR ` T ) ) ) -> ( ran ( 2nd ` <. ( ( mType ` T ) ` x ) , ( f ` <" x "> ) >. ) i^i ( mVR ` T ) ) = ( ran ( f ` <" x "> ) i^i ( mVR ` T ) ) )
103 79 97 102 3eqtrd 
 |-  ( ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) /\ x e. ( ran ( 2nd ` X ) i^i ( mVR ` T ) ) ) -> ( V ` ( ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ` ( H ` x ) ) ) = ( ran ( f ` <" x "> ) i^i ( mVR ` T ) ) )
104 103 iuneq2dv 
 |-  ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) -> U_ x e. ( ran ( 2nd ` X ) i^i ( mVR ` T ) ) ( V ` ( ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ` ( H ` x ) ) ) = U_ x e. ( ran ( 2nd ` X ) i^i ( mVR ` T ) ) ( ran ( f ` <" x "> ) i^i ( mVR ` T ) ) )
105 53 104 eqtrd 
 |-  ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) -> U_ x e. ( V ` X ) ( V ` ( ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ` ( H ` x ) ) ) = U_ x e. ( ran ( 2nd ` X ) i^i ( mVR ` T ) ) ( ran ( f ` <" x "> ) i^i ( mVR ` T ) ) )
106 23 50 105 3eqtr4d 
 |-  ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) -> ( V ` ( ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ` X ) ) = U_ x e. ( V ` X ) ( V ` ( ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ` ( H ` x ) ) ) )
107 fveq1 
 |-  ( F = ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) -> ( F ` X ) = ( ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ` X ) )
108 107 fveq2d 
 |-  ( F = ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) -> ( V ` ( F ` X ) ) = ( V ` ( ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ` X ) ) )
109 fveq1 
 |-  ( F = ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) -> ( F ` ( H ` x ) ) = ( ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ` ( H ` x ) ) )
110 109 fveq2d 
 |-  ( F = ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) -> ( V ` ( F ` ( H ` x ) ) ) = ( V ` ( ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ` ( H ` x ) ) ) )
111 110 iuneq2d 
 |-  ( F = ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) -> U_ x e. ( V ` X ) ( V ` ( F ` ( H ` x ) ) ) = U_ x e. ( V ` X ) ( V ` ( ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ` ( H ` x ) ) ) )
112 108 111 eqeq12d 
 |-  ( F = ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) -> ( ( V ` ( F ` X ) ) = U_ x e. ( V ` X ) ( V ` ( F ` ( H ` x ) ) ) <-> ( V ` ( ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ` X ) ) = U_ x e. ( V ` X ) ( V ` ( ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) ` ( H ` x ) ) ) ) )
113 106 112 syl5ibrcom 
 |-  ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) /\ X e. E ) -> ( F = ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) -> ( V ` ( F ` X ) ) = U_ x e. ( V ` X ) ( V ` ( F ` ( H ` x ) ) ) ) )
114 113 3expia 
 |-  ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) ) -> ( X e. E -> ( F = ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) -> ( V ` ( F ` X ) ) = U_ x e. ( V ` X ) ( V ` ( F ` ( H ` x ) ) ) ) ) )
115 114 com23 
 |-  ( ( T e. mFS /\ f e. ran ( mRSubst ` T ) ) -> ( F = ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) -> ( X e. E -> ( V ` ( F ` X ) ) = U_ x e. ( V ` X ) ( V ` ( F ` ( H ` x ) ) ) ) ) )
116 115 rexlimdva 
 |-  ( T e. mFS -> ( E. f e. ran ( mRSubst ` T ) F = ( e e. E |-> <. ( 1st ` e ) , ( f ` ( 2nd ` e ) ) >. ) -> ( X e. E -> ( V ` ( F ` X ) ) = U_ x e. ( V ` X ) ( V ` ( F ` ( H ` x ) ) ) ) ) )
117 12 116 syl5bi 
 |-  ( T e. mFS -> ( F e. ran S -> ( X e. E -> ( V ` ( F ` X ) ) = U_ x e. ( V ` X ) ( V ` ( F ` ( H ` x ) ) ) ) ) )
118 117 3imp 
 |-  ( ( T e. mFS /\ F e. ran S /\ X e. E ) -> ( V ` ( F ` X ) ) = U_ x e. ( V ` X ) ( V ` ( F ` ( H ` x ) ) ) )