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=mRSubstT
mrsubvrs.v V=mVRT
mrsubvrs.r R=mRExT
Assertion mrsubvrs FranSXRranFXV=xranXVranF⟨“x”⟩V

Proof

Step Hyp Ref Expression
1 mrsubco.s S=mRSubstT
2 mrsubvrs.v V=mVRT
3 mrsubvrs.r R=mRExT
4 n0i FranS¬ranS=
5 1 rnfvprc ¬TVranS=
6 4 5 nsyl2 FranSTV
7 eqid mCNT=mCNT
8 7 2 3 mrexval TVR=WordmCNTV
9 6 8 syl FranSR=WordmCNTV
10 9 eleq2d FranSXRXWordmCNTV
11 fveq2 v=Fv=F
12 11 rneqd v=ranFv=ranF
13 12 ineq1d v=ranFvV=ranFV
14 rneq v=ranv=ran
15 rn0 ran=
16 14 15 eqtrdi v=ranv=
17 16 ineq1d v=ranvV=V
18 0in V=
19 17 18 eqtrdi v=ranvV=
20 19 iuneq1d v=xranvVranF⟨“x”⟩V=xranF⟨“x”⟩V
21 0iun xranF⟨“x”⟩V=
22 20 21 eqtrdi v=xranvVranF⟨“x”⟩V=
23 13 22 eqeq12d v=ranFvV=xranvVranF⟨“x”⟩VranFV=
24 23 imbi2d v=FranSranFvV=xranvVranF⟨“x”⟩VFranSranFV=
25 fveq2 v=yFv=Fy
26 25 rneqd v=yranFv=ranFy
27 26 ineq1d v=yranFvV=ranFyV
28 rneq v=yranv=rany
29 28 ineq1d v=yranvV=ranyV
30 29 iuneq1d v=yxranvVranF⟨“x”⟩V=xranyVranF⟨“x”⟩V
31 27 30 eqeq12d v=yranFvV=xranvVranF⟨“x”⟩VranFyV=xranyVranF⟨“x”⟩V
32 31 imbi2d v=yFranSranFvV=xranvVranF⟨“x”⟩VFranSranFyV=xranyVranF⟨“x”⟩V
33 fveq2 v=y++⟨“z”⟩Fv=Fy++⟨“z”⟩
34 33 rneqd v=y++⟨“z”⟩ranFv=ranFy++⟨“z”⟩
35 34 ineq1d v=y++⟨“z”⟩ranFvV=ranFy++⟨“z”⟩V
36 rneq v=y++⟨“z”⟩ranv=rany++⟨“z”⟩
37 36 ineq1d v=y++⟨“z”⟩ranvV=rany++⟨“z”⟩V
38 37 iuneq1d v=y++⟨“z”⟩xranvVranF⟨“x”⟩V=xrany++⟨“z”⟩VranF⟨“x”⟩V
39 35 38 eqeq12d v=y++⟨“z”⟩ranFvV=xranvVranF⟨“x”⟩VranFy++⟨“z”⟩V=xrany++⟨“z”⟩VranF⟨“x”⟩V
40 39 imbi2d v=y++⟨“z”⟩FranSranFvV=xranvVranF⟨“x”⟩VFranSranFy++⟨“z”⟩V=xrany++⟨“z”⟩VranF⟨“x”⟩V
41 fveq2 v=XFv=FX
42 41 rneqd v=XranFv=ranFX
43 42 ineq1d v=XranFvV=ranFXV
44 rneq v=Xranv=ranX
45 44 ineq1d v=XranvV=ranXV
46 45 iuneq1d v=XxranvVranF⟨“x”⟩V=xranXVranF⟨“x”⟩V
47 43 46 eqeq12d v=XranFvV=xranvVranF⟨“x”⟩VranFXV=xranXVranF⟨“x”⟩V
48 47 imbi2d v=XFranSranFvV=xranvVranF⟨“x”⟩VFranSranFXV=xranXVranF⟨“x”⟩V
49 1 mrsub0 FranSF=
50 49 rneqd FranSranF=ran
51 50 15 eqtrdi FranSranF=
52 51 ineq1d FranSranFV=V
53 52 18 eqtrdi FranSranFV=
54 uneq1 ranFyV=xranyVranF⟨“x”⟩VranFyVranF⟨“z”⟩V=xranyVranF⟨“x”⟩VranF⟨“z”⟩V
55 simpl FranSyWordmCNTVzmCNTVFranS
56 simprl FranSyWordmCNTVzmCNTVyWordmCNTV
57 9 adantr FranSyWordmCNTVzmCNTVR=WordmCNTV
58 56 57 eleqtrrd FranSyWordmCNTVzmCNTVyR
59 simprr FranSyWordmCNTVzmCNTVzmCNTV
60 59 s1cld FranSyWordmCNTVzmCNTV⟨“z”⟩WordmCNTV
61 60 57 eleqtrrd FranSyWordmCNTVzmCNTV⟨“z”⟩R
62 1 3 mrsubccat FranSyR⟨“z”⟩RFy++⟨“z”⟩=Fy++F⟨“z”⟩
63 55 58 61 62 syl3anc FranSyWordmCNTVzmCNTVFy++⟨“z”⟩=Fy++F⟨“z”⟩
64 63 rneqd FranSyWordmCNTVzmCNTVranFy++⟨“z”⟩=ranFy++F⟨“z”⟩
65 1 3 mrsubf FranSF:RR
66 65 adantr FranSyWordmCNTVzmCNTVF:RR
67 66 58 ffvelrnd FranSyWordmCNTVzmCNTVFyR
68 67 57 eleqtrd FranSyWordmCNTVzmCNTVFyWordmCNTV
69 66 61 ffvelrnd FranSyWordmCNTVzmCNTVF⟨“z”⟩R
70 69 57 eleqtrd FranSyWordmCNTVzmCNTVF⟨“z”⟩WordmCNTV
71 ccatrn FyWordmCNTVF⟨“z”⟩WordmCNTVranFy++F⟨“z”⟩=ranFyranF⟨“z”⟩
72 68 70 71 syl2anc FranSyWordmCNTVzmCNTVranFy++F⟨“z”⟩=ranFyranF⟨“z”⟩
73 64 72 eqtrd FranSyWordmCNTVzmCNTVranFy++⟨“z”⟩=ranFyranF⟨“z”⟩
74 73 ineq1d FranSyWordmCNTVzmCNTVranFy++⟨“z”⟩V=ranFyranF⟨“z”⟩V
75 indir ranFyranF⟨“z”⟩V=ranFyVranF⟨“z”⟩V
76 74 75 eqtrdi FranSyWordmCNTVzmCNTVranFy++⟨“z”⟩V=ranFyVranF⟨“z”⟩V
77 ccatrn yWordmCNTV⟨“z”⟩WordmCNTVrany++⟨“z”⟩=ranyran⟨“z”⟩
78 56 60 77 syl2anc FranSyWordmCNTVzmCNTVrany++⟨“z”⟩=ranyran⟨“z”⟩
79 s1rn zmCNTVran⟨“z”⟩=z
80 79 ad2antll FranSyWordmCNTVzmCNTVran⟨“z”⟩=z
81 80 uneq2d FranSyWordmCNTVzmCNTVranyran⟨“z”⟩=ranyz
82 78 81 eqtrd FranSyWordmCNTVzmCNTVrany++⟨“z”⟩=ranyz
83 82 ineq1d FranSyWordmCNTVzmCNTVrany++⟨“z”⟩V=ranyzV
84 indir ranyzV=ranyVzV
85 83 84 eqtrdi FranSyWordmCNTVzmCNTVrany++⟨“z”⟩V=ranyVzV
86 85 iuneq1d FranSyWordmCNTVzmCNTVxrany++⟨“z”⟩VranF⟨“x”⟩V=xranyVzVranF⟨“x”⟩V
87 iunxun xranyVzVranF⟨“x”⟩V=xranyVranF⟨“x”⟩VxzVranF⟨“x”⟩V
88 86 87 eqtrdi FranSyWordmCNTVzmCNTVxrany++⟨“z”⟩VranF⟨“x”⟩V=xranyVranF⟨“x”⟩VxzVranF⟨“x”⟩V
89 simpr FranSyWordmCNTVzmCNTVzVzV
90 89 snssd FranSyWordmCNTVzmCNTVzVzV
91 df-ss zVzV=z
92 90 91 sylib FranSyWordmCNTVzmCNTVzVzV=z
93 92 iuneq1d FranSyWordmCNTVzmCNTVzVxzVranF⟨“x”⟩V=xzranF⟨“x”⟩V
94 vex zV
95 s1eq x=z⟨“x”⟩=⟨“z”⟩
96 95 fveq2d x=zF⟨“x”⟩=F⟨“z”⟩
97 96 rneqd x=zranF⟨“x”⟩=ranF⟨“z”⟩
98 97 ineq1d x=zranF⟨“x”⟩V=ranF⟨“z”⟩V
99 94 98 iunxsn xzranF⟨“x”⟩V=ranF⟨“z”⟩V
100 93 99 eqtrdi FranSyWordmCNTVzmCNTVzVxzVranF⟨“x”⟩V=ranF⟨“z”⟩V
101 incom zV=Vz
102 simpr FranSyWordmCNTVzmCNTV¬zV¬zV
103 disjsn Vz=¬zV
104 102 103 sylibr FranSyWordmCNTVzmCNTV¬zVVz=
105 101 104 eqtrid FranSyWordmCNTVzmCNTV¬zVzV=
106 105 iuneq1d FranSyWordmCNTVzmCNTV¬zVxzVranF⟨“x”⟩V=xranF⟨“x”⟩V
107 55 adantr FranSyWordmCNTVzmCNTV¬zVFranS
108 eldif zmCNTVVzmCNTV¬zV
109 108 biimpri zmCNTV¬zVzmCNTVV
110 59 109 sylan FranSyWordmCNTVzmCNTV¬zVzmCNTVV
111 difun2 mCNTVV=mCNTV
112 110 111 eleqtrdi FranSyWordmCNTVzmCNTV¬zVzmCNTV
113 1 3 2 7 mrsubcn FranSzmCNTVF⟨“z”⟩=⟨“z”⟩
114 107 112 113 syl2anc FranSyWordmCNTVzmCNTV¬zVF⟨“z”⟩=⟨“z”⟩
115 114 rneqd FranSyWordmCNTVzmCNTV¬zVranF⟨“z”⟩=ran⟨“z”⟩
116 80 adantr FranSyWordmCNTVzmCNTV¬zVran⟨“z”⟩=z
117 115 116 eqtrd FranSyWordmCNTVzmCNTV¬zVranF⟨“z”⟩=z
118 117 ineq1d FranSyWordmCNTVzmCNTV¬zVranF⟨“z”⟩V=zV
119 118 105 eqtrd FranSyWordmCNTVzmCNTV¬zVranF⟨“z”⟩V=
120 21 106 119 3eqtr4a FranSyWordmCNTVzmCNTV¬zVxzVranF⟨“x”⟩V=ranF⟨“z”⟩V
121 100 120 pm2.61dan FranSyWordmCNTVzmCNTVxzVranF⟨“x”⟩V=ranF⟨“z”⟩V
122 121 uneq2d FranSyWordmCNTVzmCNTVxranyVranF⟨“x”⟩VxzVranF⟨“x”⟩V=xranyVranF⟨“x”⟩VranF⟨“z”⟩V
123 88 122 eqtrd FranSyWordmCNTVzmCNTVxrany++⟨“z”⟩VranF⟨“x”⟩V=xranyVranF⟨“x”⟩VranF⟨“z”⟩V
124 76 123 eqeq12d FranSyWordmCNTVzmCNTVranFy++⟨“z”⟩V=xrany++⟨“z”⟩VranF⟨“x”⟩VranFyVranF⟨“z”⟩V=xranyVranF⟨“x”⟩VranF⟨“z”⟩V
125 54 124 syl5ibr FranSyWordmCNTVzmCNTVranFyV=xranyVranF⟨“x”⟩VranFy++⟨“z”⟩V=xrany++⟨“z”⟩VranF⟨“x”⟩V
126 125 expcom yWordmCNTVzmCNTVFranSranFyV=xranyVranF⟨“x”⟩VranFy++⟨“z”⟩V=xrany++⟨“z”⟩VranF⟨“x”⟩V
127 126 a2d yWordmCNTVzmCNTVFranSranFyV=xranyVranF⟨“x”⟩VFranSranFy++⟨“z”⟩V=xrany++⟨“z”⟩VranF⟨“x”⟩V
128 24 32 40 48 53 127 wrdind XWordmCNTVFranSranFXV=xranXVranF⟨“x”⟩V
129 128 com12 FranSXWordmCNTVranFXV=xranXVranF⟨“x”⟩V
130 10 129 sylbid FranSXRranFXV=xranXVranF⟨“x”⟩V
131 130 imp FranSXRranFXV=xranXVranF⟨“x”⟩V