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 ⊢ 𝑆 = ( mRSubst ‘ 𝑇 )
mrsubvrs.v ⊢ 𝑉 = ( mVR ‘ 𝑇 )
mrsubvrs.r ⊢ 𝑅 = ( mREx ‘ 𝑇 )
Assertion mrsubvrs ( ( 𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ 𝑅 ) → ( ran ( 𝐹 ‘ 𝑋 ) ∩ 𝑉 ) = ∪ 𝑥 ∈ ( ran 𝑋 ∩ 𝑉 ) ( ran ( 𝐹 ‘ ⟨“ 𝑥 ”⟩ ) ∩ 𝑉 ) )

Proof

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