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