# 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}=\mathrm{mRSubst}\left({T}\right)$
mrsubvrs.v ${⊢}{V}=\mathrm{mVR}\left({T}\right)$
mrsubvrs.r ${⊢}{R}=\mathrm{mREx}\left({T}\right)$
Assertion mrsubvrs ${⊢}\left({F}\in \mathrm{ran}{S}\wedge {X}\in {R}\right)\to \mathrm{ran}{F}\left({X}\right)\cap {V}=\bigcup _{{x}\in \mathrm{ran}{X}\cap {V}}\left(\mathrm{ran}{F}\left(⟨“{x}”⟩\right)\cap {V}\right)$

### Proof

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