Metamath Proof Explorer


Theorem mrsubvrs

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 mrsubco.s S = mRSubst T
mrsubvrs.v V = mVR T
mrsubvrs.r R = mREx T
Assertion mrsubvrs F ran S X R ran F X V = x ran X V ran F ⟨“ x ”⟩ V

Proof

Step Hyp Ref Expression
1 mrsubco.s S = mRSubst T
2 mrsubvrs.v V = mVR T
3 mrsubvrs.r R = mREx T
4 n0i F ran S ¬ ran S =
5 1 rnfvprc ¬ T V ran S =
6 4 5 nsyl2 F ran S T V
7 eqid mCN T = mCN T
8 7 2 3 mrexval T V R = Word mCN T V
9 6 8 syl F ran S R = Word mCN T V
10 9 eleq2d F ran S X R X Word mCN T V
11 fveq2 v = F v = F
12 11 rneqd v = ran F v = ran F
13 12 ineq1d v = ran F v V = ran F V
14 rneq v = ran v = ran
15 rn0 ran =
16 14 15 eqtrdi v = ran v =
17 16 ineq1d v = ran v V = V
18 0in V =
19 17 18 eqtrdi v = ran v V =
20 19 iuneq1d v = x ran v V ran F ⟨“ x ”⟩ V = x ran F ⟨“ x ”⟩ V
21 0iun x ran F ⟨“ x ”⟩ V =
22 20 21 eqtrdi v = x ran v V ran F ⟨“ x ”⟩ V =
23 13 22 eqeq12d v = ran F v V = x ran v V ran F ⟨“ x ”⟩ V ran F V =
24 23 imbi2d v = F ran S ran F v V = x ran v V ran F ⟨“ x ”⟩ V F ran S ran F V =
25 fveq2 v = y F v = F y
26 25 rneqd v = y ran F v = ran F y
27 26 ineq1d v = y ran F v V = ran F y V
28 rneq v = y ran v = ran y
29 28 ineq1d v = y ran v V = ran y V
30 29 iuneq1d v = y x ran v V ran F ⟨“ x ”⟩ V = x ran y V ran F ⟨“ x ”⟩ V
31 27 30 eqeq12d v = y ran F v V = x ran v V ran F ⟨“ x ”⟩ V ran F y V = x ran y V ran F ⟨“ x ”⟩ V
32 31 imbi2d v = y F ran S ran F v V = x ran v V ran F ⟨“ x ”⟩ V F ran S ran F y V = x ran y V ran F ⟨“ x ”⟩ V
33 fveq2 v = y ++ ⟨“ z ”⟩ F v = F y ++ ⟨“ z ”⟩
34 33 rneqd v = y ++ ⟨“ z ”⟩ ran F v = ran F y ++ ⟨“ z ”⟩
35 34 ineq1d v = y ++ ⟨“ z ”⟩ ran F v V = ran F y ++ ⟨“ z ”⟩ V
36 rneq v = y ++ ⟨“ z ”⟩ ran v = ran y ++ ⟨“ z ”⟩
37 36 ineq1d v = y ++ ⟨“ z ”⟩ ran v V = ran y ++ ⟨“ z ”⟩ V
38 37 iuneq1d v = y ++ ⟨“ z ”⟩ x ran v V ran F ⟨“ x ”⟩ V = x ran y ++ ⟨“ z ”⟩ V ran F ⟨“ x ”⟩ V
39 35 38 eqeq12d v = y ++ ⟨“ z ”⟩ ran F v V = x ran v V ran F ⟨“ x ”⟩ V ran F y ++ ⟨“ z ”⟩ V = x ran y ++ ⟨“ z ”⟩ V ran F ⟨“ x ”⟩ V
40 39 imbi2d v = y ++ ⟨“ z ”⟩ F ran S ran F v V = x ran v V ran F ⟨“ x ”⟩ V F ran S ran F y ++ ⟨“ z ”⟩ V = x ran y ++ ⟨“ z ”⟩ V ran F ⟨“ x ”⟩ V
41 fveq2 v = X F v = F X
42 41 rneqd v = X ran F v = ran F X
43 42 ineq1d v = X ran F v V = ran F X V
44 rneq v = X ran v = ran X
45 44 ineq1d v = X ran v V = ran X V
46 45 iuneq1d v = X x ran v V ran F ⟨“ x ”⟩ V = x ran X V ran F ⟨“ x ”⟩ V
47 43 46 eqeq12d v = X ran F v V = x ran v V ran F ⟨“ x ”⟩ V ran F X V = x ran X V ran F ⟨“ x ”⟩ V
48 47 imbi2d v = X F ran S ran F v V = x ran v V ran F ⟨“ x ”⟩ V F ran S ran F X V = x ran X V ran F ⟨“ x ”⟩ V
49 1 mrsub0 F ran S F =
50 49 rneqd F ran S ran F = ran
51 50 15 eqtrdi F ran S ran F =
52 51 ineq1d F ran S ran F V = V
53 52 18 eqtrdi F ran S ran F V =
54 uneq1 ran F y V = x ran y V ran F ⟨“ x ”⟩ V ran F y V ran F ⟨“ z ”⟩ V = x ran y V ran F ⟨“ x ”⟩ V ran F ⟨“ z ”⟩ V
55 simpl F ran S y Word mCN T V z mCN T V F ran S
56 simprl F ran S y Word mCN T V z mCN T V y Word mCN T V
57 9 adantr F ran S y Word mCN T V z mCN T V R = Word mCN T V
58 56 57 eleqtrrd F ran S y Word mCN T V z mCN T V y R
59 simprr F ran S y Word mCN T V z mCN T V z mCN T V
60 59 s1cld F ran S y Word mCN T V z mCN T V ⟨“ z ”⟩ Word mCN T V
61 60 57 eleqtrrd F ran S y Word mCN T V z mCN T V ⟨“ z ”⟩ R
62 1 3 mrsubccat F ran S y R ⟨“ z ”⟩ R F y ++ ⟨“ z ”⟩ = F y ++ F ⟨“ z ”⟩
63 55 58 61 62 syl3anc F ran S y Word mCN T V z mCN T V F y ++ ⟨“ z ”⟩ = F y ++ F ⟨“ z ”⟩
64 63 rneqd F ran S y Word mCN T V z mCN T V ran F y ++ ⟨“ z ”⟩ = ran F y ++ F ⟨“ z ”⟩
65 1 3 mrsubf F ran S F : R R
66 65 adantr F ran S y Word mCN T V z mCN T V F : R R
67 66 58 ffvelrnd F ran S y Word mCN T V z mCN T V F y R
68 67 57 eleqtrd F ran S y Word mCN T V z mCN T V F y Word mCN T V
69 66 61 ffvelrnd F ran S y Word mCN T V z mCN T V F ⟨“ z ”⟩ R
70 69 57 eleqtrd F ran S y Word mCN T V z mCN T V F ⟨“ z ”⟩ Word mCN T V
71 ccatrn F y Word mCN T V F ⟨“ z ”⟩ Word mCN T V ran F y ++ F ⟨“ z ”⟩ = ran F y ran F ⟨“ z ”⟩
72 68 70 71 syl2anc F ran S y Word mCN T V z mCN T V ran F y ++ F ⟨“ z ”⟩ = ran F y ran F ⟨“ z ”⟩
73 64 72 eqtrd F ran S y Word mCN T V z mCN T V ran F y ++ ⟨“ z ”⟩ = ran F y ran F ⟨“ z ”⟩
74 73 ineq1d F ran S y Word mCN T V z mCN T V ran F y ++ ⟨“ z ”⟩ V = ran F y ran F ⟨“ z ”⟩ V
75 indir ran F y ran F ⟨“ z ”⟩ V = ran F y V ran F ⟨“ z ”⟩ V
76 74 75 eqtrdi F ran S y Word mCN T V z mCN T V ran F y ++ ⟨“ z ”⟩ V = ran F y V ran F ⟨“ z ”⟩ V
77 ccatrn y Word mCN T V ⟨“ z ”⟩ Word mCN T V ran y ++ ⟨“ z ”⟩ = ran y ran ⟨“ z ”⟩
78 56 60 77 syl2anc F ran S y Word mCN T V z mCN T V ran y ++ ⟨“ z ”⟩ = ran y ran ⟨“ z ”⟩
79 s1rn z mCN T V ran ⟨“ z ”⟩ = z
80 79 ad2antll F ran S y Word mCN T V z mCN T V ran ⟨“ z ”⟩ = z
81 80 uneq2d F ran S y Word mCN T V z mCN T V ran y ran ⟨“ z ”⟩ = ran y z
82 78 81 eqtrd F ran S y Word mCN T V z mCN T V ran y ++ ⟨“ z ”⟩ = ran y z
83 82 ineq1d F ran S y Word mCN T V z mCN T V ran y ++ ⟨“ z ”⟩ V = ran y z V
84 indir ran y z V = ran y V z V
85 83 84 eqtrdi F ran S y Word mCN T V z mCN T V ran y ++ ⟨“ z ”⟩ V = ran y V z V
86 85 iuneq1d F ran S y Word mCN T V z mCN T V x ran y ++ ⟨“ z ”⟩ V ran F ⟨“ x ”⟩ V = x ran y V z V ran F ⟨“ x ”⟩ V
87 iunxun x ran y V z V ran F ⟨“ x ”⟩ V = x ran y V ran F ⟨“ x ”⟩ V x z V ran F ⟨“ x ”⟩ V
88 86 87 eqtrdi F ran S y Word mCN T V z mCN T V x ran y ++ ⟨“ z ”⟩ V ran F ⟨“ x ”⟩ V = x ran y V ran F ⟨“ x ”⟩ V x z V ran F ⟨“ x ”⟩ V
89 simpr F ran S y Word mCN T V z mCN T V z V z V
90 89 snssd F ran S y Word mCN T V z mCN T V z V z V
91 df-ss z V z V = z
92 90 91 sylib F ran S y Word mCN T V z mCN T V z V z V = z
93 92 iuneq1d F ran S y Word mCN T V z mCN T V z V x z V ran F ⟨“ x ”⟩ V = x z ran F ⟨“ x ”⟩ V
94 vex z V
95 s1eq x = z ⟨“ x ”⟩ = ⟨“ z ”⟩
96 95 fveq2d x = z F ⟨“ x ”⟩ = F ⟨“ z ”⟩
97 96 rneqd x = z ran F ⟨“ x ”⟩ = ran F ⟨“ z ”⟩
98 97 ineq1d x = z ran F ⟨“ x ”⟩ V = ran F ⟨“ z ”⟩ V
99 94 98 iunxsn x z ran F ⟨“ x ”⟩ V = ran F ⟨“ z ”⟩ V
100 93 99 eqtrdi F ran S y Word mCN T V z mCN T V z V x z V ran F ⟨“ x ”⟩ V = ran F ⟨“ z ”⟩ V
101 incom z V = V z
102 simpr F ran S y Word mCN T V z mCN T V ¬ z V ¬ z V
103 disjsn V z = ¬ z V
104 102 103 sylibr F ran S y Word mCN T V z mCN T V ¬ z V V z =
105 101 104 syl5eq F ran S y Word mCN T V z mCN T V ¬ z V z V =
106 105 iuneq1d F ran S y Word mCN T V z mCN T V ¬ z V x z V ran F ⟨“ x ”⟩ V = x ran F ⟨“ x ”⟩ V
107 55 adantr F ran S y Word mCN T V z mCN T V ¬ z V F ran S
108 eldif z mCN T V V z mCN T V ¬ z V
109 108 biimpri z mCN T V ¬ z V z mCN T V V
110 59 109 sylan F ran S y Word mCN T V z mCN T V ¬ z V z mCN T V V
111 difun2 mCN T V V = mCN T V
112 110 111 eleqtrdi F ran S y Word mCN T V z mCN T V ¬ z V z mCN T V
113 1 3 2 7 mrsubcn F ran S z mCN T V F ⟨“ z ”⟩ = ⟨“ z ”⟩
114 107 112 113 syl2anc F ran S y Word mCN T V z mCN T V ¬ z V F ⟨“ z ”⟩ = ⟨“ z ”⟩
115 114 rneqd F ran S y Word mCN T V z mCN T V ¬ z V ran F ⟨“ z ”⟩ = ran ⟨“ z ”⟩
116 80 adantr F ran S y Word mCN T V z mCN T V ¬ z V ran ⟨“ z ”⟩ = z
117 115 116 eqtrd F ran S y Word mCN T V z mCN T V ¬ z V ran F ⟨“ z ”⟩ = z
118 117 ineq1d F ran S y Word mCN T V z mCN T V ¬ z V ran F ⟨“ z ”⟩ V = z V
119 118 105 eqtrd F ran S y Word mCN T V z mCN T V ¬ z V ran F ⟨“ z ”⟩ V =
120 21 106 119 3eqtr4a F ran S y Word mCN T V z mCN T V ¬ z V x z V ran F ⟨“ x ”⟩ V = ran F ⟨“ z ”⟩ V
121 100 120 pm2.61dan F ran S y Word mCN T V z mCN T V x z V ran F ⟨“ x ”⟩ V = ran F ⟨“ z ”⟩ V
122 121 uneq2d F ran S y Word mCN T V z mCN T V x ran y V ran F ⟨“ x ”⟩ V x z V ran F ⟨“ x ”⟩ V = x ran y V ran F ⟨“ x ”⟩ V ran F ⟨“ z ”⟩ V
123 88 122 eqtrd F ran S y Word mCN T V z mCN T V x ran y ++ ⟨“ z ”⟩ V ran F ⟨“ x ”⟩ V = x ran y V ran F ⟨“ x ”⟩ V ran F ⟨“ z ”⟩ V
124 76 123 eqeq12d F ran S y Word mCN T V z mCN T V ran F y ++ ⟨“ z ”⟩ V = x ran y ++ ⟨“ z ”⟩ V ran F ⟨“ x ”⟩ V ran F y V ran F ⟨“ z ”⟩ V = x ran y V ran F ⟨“ x ”⟩ V ran F ⟨“ z ”⟩ V
125 54 124 syl5ibr F ran S y Word mCN T V z mCN T V ran F y V = x ran y V ran F ⟨“ x ”⟩ V ran F y ++ ⟨“ z ”⟩ V = x ran y ++ ⟨“ z ”⟩ V ran F ⟨“ x ”⟩ V
126 125 expcom y Word mCN T V z mCN T V F ran S ran F y V = x ran y V ran F ⟨“ x ”⟩ V ran F y ++ ⟨“ z ”⟩ V = x ran y ++ ⟨“ z ”⟩ V ran F ⟨“ x ”⟩ V
127 126 a2d y Word mCN T V z mCN T V F ran S ran F y V = x ran y V ran F ⟨“ x ”⟩ V F ran S ran F y ++ ⟨“ z ”⟩ V = x ran y ++ ⟨“ z ”⟩ V ran F ⟨“ x ”⟩ V
128 24 32 40 48 53 127 wrdind X Word mCN T V F ran S ran F X V = x ran X V ran F ⟨“ x ”⟩ V
129 128 com12 F ran S X Word mCN T V ran F X V = x ran X V ran F ⟨“ x ”⟩ V
130 10 129 sylbid F ran S X R ran F X V = x ran X V ran F ⟨“ x ”⟩ V
131 130 imp F ran S X R ran F X V = x ran X V ran F ⟨“ x ”⟩ V