Metamath Proof Explorer

Theorem cycpmco2

Description: The composition of a cyclic permutation and a transposition of one element in the cycle and one outside the cycle results in a cyclic permutation with one more element in its orbit. (Contributed by Thierry Arnoux, 2-Jan-2024)

Ref Expression
Hypotheses cycpmco2.c ⊢ 𝑀 = ( toCyc ‘ 𝐷 )
cycpmco2.s ⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
cycpmco2.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
cycpmco2.w ⊢ ( 𝜑 → 𝑊 ∈ dom 𝑀 )
cycpmco2.i ⊢ ( 𝜑 → 𝐼 ∈ ( 𝐷 ∖ ran 𝑊 ) )
cycpmco2.j ⊢ ( 𝜑 → 𝐽 ∈ ran 𝑊 )
cycpmco2.e ⊢ 𝐸 = ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 )
cycpmco2.1 ⊢ 𝑈 = ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ )
Assertion cycpmco2 ( 𝜑 → ( ( 𝑀 ‘ 𝑊 ) ∘ ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ) = ( 𝑀 ‘ 𝑈 ) )

Proof

Step Hyp Ref Expression
1 cycpmco2.c ⊢ 𝑀 = ( toCyc ‘ 𝐷 )
2 cycpmco2.s ⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
3 cycpmco2.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
4 cycpmco2.w ⊢ ( 𝜑 → 𝑊 ∈ dom 𝑀 )
5 cycpmco2.i ⊢ ( 𝜑 → 𝐼 ∈ ( 𝐷 ∖ ran 𝑊 ) )
6 cycpmco2.j ⊢ ( 𝜑 → 𝐽 ∈ ran 𝑊 )
7 cycpmco2.e ⊢ 𝐸 = ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 )
8 cycpmco2.1 ⊢ 𝑈 = ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ )
9 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
10 1 2 9 tocycf ⊢ ( 𝐷 ∈ 𝑉 → 𝑀 : { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ⟶ ( Base ‘ 𝑆 ) )
11 3 10 syl ⊢ ( 𝜑 → 𝑀 : { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ⟶ ( Base ‘ 𝑆 ) )
12 11 fdmd ⊢ ( 𝜑 → dom 𝑀 = { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } )
13 4 12 eleqtrd ⊢ ( 𝜑 → 𝑊 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } )
14 11 13 ffvelcdmd ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑊 ) ∈ ( Base ‘ 𝑆 ) )
15 2 9 symgbasf ⊢ ( ( 𝑀 ‘ 𝑊 ) ∈ ( Base ‘ 𝑆 ) → ( 𝑀 ‘ 𝑊 ) : 𝐷 ⟶ 𝐷 )
16 14 15 syl ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑊 ) : 𝐷 ⟶ 𝐷 )
17 16 ffnd ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑊 ) Fn 𝐷 )
18 5 eldifad ⊢ ( 𝜑 → 𝐼 ∈ 𝐷 )
19 ssrab2 ⊢ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ⊆ Word 𝐷
20 19 13 sselid ⊢ ( 𝜑 → 𝑊 ∈ Word 𝐷 )
21 id ⊢ ( 𝑤 = 𝑊 → 𝑤 = 𝑊 )
22 dmeq ⊢ ( 𝑤 = 𝑊 → dom 𝑤 = dom 𝑊 )
23 eqidd ⊢ ( 𝑤 = 𝑊 → 𝐷 = 𝐷 )
24 21 22 23 f1eq123d ⊢ ( 𝑤 = 𝑊 → ( 𝑤 : dom 𝑤 –1-1→ 𝐷 ↔ 𝑊 : dom 𝑊 –1-1→ 𝐷 ) )
25 24 elrab3 ⊢ ( 𝑊 ∈ Word 𝐷 → ( 𝑊 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ↔ 𝑊 : dom 𝑊 –1-1→ 𝐷 ) )
26 25 biimpa ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 𝑊 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ) → 𝑊 : dom 𝑊 –1-1→ 𝐷 )
27 20 13 26 syl2anc ⊢ ( 𝜑 → 𝑊 : dom 𝑊 –1-1→ 𝐷 )
28 f1f ⊢ ( 𝑊 : dom 𝑊 –1-1→ 𝐷 → 𝑊 : dom 𝑊 ⟶ 𝐷 )
29 27 28 syl ⊢ ( 𝜑 → 𝑊 : dom 𝑊 ⟶ 𝐷 )
30 29 frnd ⊢ ( 𝜑 → ran 𝑊 ⊆ 𝐷 )
31 30 6 sseldd ⊢ ( 𝜑 → 𝐽 ∈ 𝐷 )
32 5 eldifbd ⊢ ( 𝜑 → ¬ 𝐼 ∈ ran 𝑊 )
33 nelne2 ⊢ ( ( 𝐽 ∈ ran 𝑊 ∧ ¬ 𝐼 ∈ ran 𝑊 ) → 𝐽 ≠ 𝐼 )
34 6 32 33 syl2anc ⊢ ( 𝜑 → 𝐽 ≠ 𝐼 )
35 34 necomd ⊢ ( 𝜑 → 𝐼 ≠ 𝐽 )
36 1 3 18 31 35 2 cycpm2cl ⊢ ( 𝜑 → ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ∈ ( Base ‘ 𝑆 ) )
37 2 9 symgbasf ⊢ ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ∈ ( Base ‘ 𝑆 ) → ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) : 𝐷 ⟶ 𝐷 )
38 36 37 syl ⊢ ( 𝜑 → ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) : 𝐷 ⟶ 𝐷 )
39 38 ffnd ⊢ ( 𝜑 → ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) Fn 𝐷 )
40 38 frnd ⊢ ( 𝜑 → ran ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ⊆ 𝐷 )
41 fnco ⊢ ( ( ( 𝑀 ‘ 𝑊 ) Fn 𝐷 ∧ ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) Fn 𝐷 ∧ ran ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ⊆ 𝐷 ) → ( ( 𝑀 ‘ 𝑊 ) ∘ ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ) Fn 𝐷 )
42 17 39 40 41 syl3anc ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑊 ) ∘ ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ) Fn 𝐷 )
43 18 s1cld ⊢ ( 𝜑 → ⟨“ 𝐼 ”⟩ ∈ Word 𝐷 )
44 splcl ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ ⟨“ 𝐼 ”⟩ ∈ Word 𝐷 ) → ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ ) ∈ Word 𝐷 )
45 20 43 44 syl2anc ⊢ ( 𝜑 → ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ ) ∈ Word 𝐷 )
46 8 45 eqeltrid ⊢ ( 𝜑 → 𝑈 ∈ Word 𝐷 )
47 1 2 3 4 5 6 7 8 cycpmco2f1 ⊢ ( 𝜑 → 𝑈 : dom 𝑈 –1-1→ 𝐷 )
48 1 3 46 47 2 cycpmcl ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑈 ) ∈ ( Base ‘ 𝑆 ) )
49 2 9 symgbasf ⊢ ( ( 𝑀 ‘ 𝑈 ) ∈ ( Base ‘ 𝑆 ) → ( 𝑀 ‘ 𝑈 ) : 𝐷 ⟶ 𝐷 )
50 48 49 syl ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑈 ) : 𝐷 ⟶ 𝐷 )
51 50 ffnd ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑈 ) Fn 𝐷 )
52 fvco3 ⊢ ( ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) : 𝐷 ⟶ 𝐷 ∧ 𝑖 ∈ 𝐷 ) → ( ( ( 𝑀 ‘ 𝑊 ) ∘ ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ) ‘ 𝑖 ) = ( ( 𝑀 ‘ 𝑊 ) ‘ ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝑖 ) ) )
53 38 52 sylan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐷 ) → ( ( ( 𝑀 ‘ 𝑊 ) ∘ ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ) ‘ 𝑖 ) = ( ( 𝑀 ‘ 𝑊 ) ‘ ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝑖 ) ) )
54 1 3 18 31 35 2 cyc2fv2 ⊢ ( 𝜑 → ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝐽 ) = 𝐼 )
55 54 fveq2d ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑊 ) ‘ ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝐽 ) ) = ( ( 𝑀 ‘ 𝑊 ) ‘ 𝐼 ) )
56 1 2 3 4 5 6 7 8 cycpmco2lem2 ⊢ ( 𝜑 → ( 𝑈 ‘ 𝐸 ) = 𝐼 )
57 f1cnv ⊢ ( 𝑊 : dom 𝑊 –1-1→ 𝐷 → ◡ 𝑊 : ran 𝑊 –1-1-onto→ dom 𝑊 )
58 f1of ⊢ ( ◡ 𝑊 : ran 𝑊 –1-1-onto→ dom 𝑊 → ◡ 𝑊 : ran 𝑊 ⟶ dom 𝑊 )
59 27 57 58 3syl ⊢ ( 𝜑 → ◡ 𝑊 : ran 𝑊 ⟶ dom 𝑊 )
60 59 6 ffvelcdmd ⊢ ( 𝜑 → ( ◡ 𝑊 ‘ 𝐽 ) ∈ dom 𝑊 )
61 wrddm ⊢ ( 𝑊 ∈ Word 𝐷 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
62 20 61 syl ⊢ ( 𝜑 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
63 60 62 eleqtrd ⊢ ( 𝜑 → ( ◡ 𝑊 ‘ 𝐽 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
64 lencl ⊢ ( 𝑊 ∈ Word 𝐷 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
65 20 64 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
66 65 nn0cnd ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℂ )
67 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
68 ovexd ⊢ ( 𝜑 → ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) ∈ V )
69 7 68 eqeltrid ⊢ ( 𝜑 → 𝐸 ∈ V )
70 splval ⊢ ( ( 𝑊 ∈ dom 𝑀 ∧ ( 𝐸 ∈ V ∧ 𝐸 ∈ V ∧ ⟨“ 𝐼 ”⟩ ∈ Word 𝐷 ) ) → ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ ) = ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) )
71 4 69 69 43 70 syl13anc ⊢ ( 𝜑 → ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ ) = ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) )
72 8 71 eqtrid ⊢ ( 𝜑 → 𝑈 = ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) )
73 72 fveq2d ⊢ ( 𝜑 → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) )
74 pfxcl ⊢ ( 𝑊 ∈ Word 𝐷 → ( 𝑊 prefix 𝐸 ) ∈ Word 𝐷 )
75 20 74 syl ⊢ ( 𝜑 → ( 𝑊 prefix 𝐸 ) ∈ Word 𝐷 )
76 ccatcl ⊢ ( ( ( 𝑊 prefix 𝐸 ) ∈ Word 𝐷 ∧ ⟨“ 𝐼 ”⟩ ∈ Word 𝐷 ) → ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ∈ Word 𝐷 )
77 75 43 76 syl2anc ⊢ ( 𝜑 → ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ∈ Word 𝐷 )
78 swrdcl ⊢ ( 𝑊 ∈ Word 𝐷 → ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ∈ Word 𝐷 )
79 20 78 syl ⊢ ( 𝜑 → ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ∈ Word 𝐷 )
80 ccatlen ⊢ ( ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ∈ Word 𝐷 ∧ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ∈ Word 𝐷 ) → ( ♯ ‘ ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) = ( ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) + ( ♯ ‘ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) )
81 77 79 80 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) = ( ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) + ( ♯ ‘ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) )
82 ccatws1len ⊢ ( ( 𝑊 prefix 𝐸 ) ∈ Word 𝐷 → ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) = ( ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) + 1 ) )
83 20 74 82 3syl ⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) = ( ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) + 1 ) )
84 fzofzp1 ⊢ ( ( ◡ 𝑊 ‘ 𝐽 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
85 63 84 syl ⊢ ( 𝜑 → ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
86 7 85 eqeltrid ⊢ ( 𝜑 → 𝐸 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
87 pfxlen ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 𝐸 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) = 𝐸 )
88 20 86 87 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) = 𝐸 )
89 88 oveq1d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) + 1 ) = ( 𝐸 + 1 ) )
90 83 89 eqtrd ⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) = ( 𝐸 + 1 ) )
91 nn0fz0 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ↔ ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
92 65 91 sylib ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
93 swrdlen ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 𝐸 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) = ( ( ♯ ‘ 𝑊 ) − 𝐸 ) )
94 20 86 92 93 syl3anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) = ( ( ♯ ‘ 𝑊 ) − 𝐸 ) )
95 90 94 oveq12d ⊢ ( 𝜑 → ( ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) + ( ♯ ‘ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) = ( ( 𝐸 + 1 ) + ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) )
96 73 81 95 3eqtrd ⊢ ( 𝜑 → ( ♯ ‘ 𝑈 ) = ( ( 𝐸 + 1 ) + ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) )
97 fz0ssnn0 ⊢ ( 0 ... ( ♯ ‘ 𝑊 ) ) ⊆ ℕ0
98 97 86 sselid ⊢ ( 𝜑 → 𝐸 ∈ ℕ0 )
99 98 nn0zd ⊢ ( 𝜑 → 𝐸 ∈ ℤ )
100 99 peano2zd ⊢ ( 𝜑 → ( 𝐸 + 1 ) ∈ ℤ )
101 100 zcnd ⊢ ( 𝜑 → ( 𝐸 + 1 ) ∈ ℂ )
102 98 nn0cnd ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
103 101 66 102 addsubassd ⊢ ( 𝜑 → ( ( ( 𝐸 + 1 ) + ( ♯ ‘ 𝑊 ) ) − 𝐸 ) = ( ( 𝐸 + 1 ) + ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) )
104 102 67 66 addassd ⊢ ( 𝜑 → ( ( 𝐸 + 1 ) + ( ♯ ‘ 𝑊 ) ) = ( 𝐸 + ( 1 + ( ♯ ‘ 𝑊 ) ) ) )
105 104 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐸 + 1 ) + ( ♯ ‘ 𝑊 ) ) − 𝐸 ) = ( ( 𝐸 + ( 1 + ( ♯ ‘ 𝑊 ) ) ) − 𝐸 ) )
106 96 103 105 3eqtr2d ⊢ ( 𝜑 → ( ♯ ‘ 𝑈 ) = ( ( 𝐸 + ( 1 + ( ♯ ‘ 𝑊 ) ) ) − 𝐸 ) )
107 67 66 addcld ⊢ ( 𝜑 → ( 1 + ( ♯ ‘ 𝑊 ) ) ∈ ℂ )
108 102 107 pncan2d ⊢ ( 𝜑 → ( ( 𝐸 + ( 1 + ( ♯ ‘ 𝑊 ) ) ) − 𝐸 ) = ( 1 + ( ♯ ‘ 𝑊 ) ) )
109 67 66 addcomd ⊢ ( 𝜑 → ( 1 + ( ♯ ‘ 𝑊 ) ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
110 106 108 109 3eqtrd ⊢ ( 𝜑 → ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
111 66 67 110 mvrraddd ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑈 ) − 1 ) = ( ♯ ‘ 𝑊 ) )
112 111 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
113 63 112 eleqtrrd ⊢ ( 𝜑 → ( ◡ 𝑊 ‘ 𝐽 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) )
114 1 3 46 47 113 cycpmfv1 ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑈 ) ‘ ( 𝑈 ‘ ( ◡ 𝑊 ‘ 𝐽 ) ) ) = ( 𝑈 ‘ ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) ) )
115 7 fveq2i ⊢ ( 𝑈 ‘ 𝐸 ) = ( 𝑈 ‘ ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) )
116 114 115 eqtr4di ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑈 ) ‘ ( 𝑈 ‘ ( ◡ 𝑊 ‘ 𝐽 ) ) ) = ( 𝑈 ‘ 𝐸 ) )
117 1 3 20 27 18 32 cycpmfv3 ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑊 ) ‘ 𝐼 ) = 𝐼 )
118 56 116 117 3eqtr4d ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑈 ) ‘ ( 𝑈 ‘ ( ◡ 𝑊 ‘ 𝐽 ) ) ) = ( ( 𝑀 ‘ 𝑊 ) ‘ 𝐼 ) )
119 72 fveq1d ⊢ ( 𝜑 → ( 𝑈 ‘ ( ◡ 𝑊 ‘ 𝐽 ) ) = ( ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ‘ ( ◡ 𝑊 ‘ 𝐽 ) ) )
120 fzossfzop1 ⊢ ( 𝐸 ∈ ℕ0 → ( 0 ..^ 𝐸 ) ⊆ ( 0 ..^ ( 𝐸 + 1 ) ) )
121 98 120 syl ⊢ ( 𝜑 → ( 0 ..^ 𝐸 ) ⊆ ( 0 ..^ ( 𝐸 + 1 ) ) )
122 elfzonn0 ⊢ ( ( ◡ 𝑊 ‘ 𝐽 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ◡ 𝑊 ‘ 𝐽 ) ∈ ℕ0 )
123 fzonn0p1 ⊢ ( ( ◡ 𝑊 ‘ 𝐽 ) ∈ ℕ0 → ( ◡ 𝑊 ‘ 𝐽 ) ∈ ( 0 ..^ ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) ) )
124 63 122 123 3syl ⊢ ( 𝜑 → ( ◡ 𝑊 ‘ 𝐽 ) ∈ ( 0 ..^ ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) ) )
125 7 oveq2i ⊢ ( 0 ..^ 𝐸 ) = ( 0 ..^ ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) )
126 124 125 eleqtrrdi ⊢ ( 𝜑 → ( ◡ 𝑊 ‘ 𝐽 ) ∈ ( 0 ..^ 𝐸 ) )
127 121 126 sseldd ⊢ ( 𝜑 → ( ◡ 𝑊 ‘ 𝐽 ) ∈ ( 0 ..^ ( 𝐸 + 1 ) ) )
128 90 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) ) = ( 0 ..^ ( 𝐸 + 1 ) ) )
129 127 128 eleqtrrd ⊢ ( 𝜑 → ( ◡ 𝑊 ‘ 𝐽 ) ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) ) )
130 ccatval1 ⊢ ( ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ∈ Word 𝐷 ∧ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ∈ Word 𝐷 ∧ ( ◡ 𝑊 ‘ 𝐽 ) ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) ) ) → ( ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ‘ ( ◡ 𝑊 ‘ 𝐽 ) ) = ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ‘ ( ◡ 𝑊 ‘ 𝐽 ) ) )
131 77 79 129 130 syl3anc ⊢ ( 𝜑 → ( ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ‘ ( ◡ 𝑊 ‘ 𝐽 ) ) = ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ‘ ( ◡ 𝑊 ‘ 𝐽 ) ) )
132 88 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) ) = ( 0 ..^ 𝐸 ) )
133 126 132 eleqtrrd ⊢ ( 𝜑 → ( ◡ 𝑊 ‘ 𝐽 ) ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) ) )
134 ccatval1 ⊢ ( ( ( 𝑊 prefix 𝐸 ) ∈ Word 𝐷 ∧ ⟨“ 𝐼 ”⟩ ∈ Word 𝐷 ∧ ( ◡ 𝑊 ‘ 𝐽 ) ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) ) ) → ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ‘ ( ◡ 𝑊 ‘ 𝐽 ) ) = ( ( 𝑊 prefix 𝐸 ) ‘ ( ◡ 𝑊 ‘ 𝐽 ) ) )
135 75 43 133 134 syl3anc ⊢ ( 𝜑 → ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ‘ ( ◡ 𝑊 ‘ 𝐽 ) ) = ( ( 𝑊 prefix 𝐸 ) ‘ ( ◡ 𝑊 ‘ 𝐽 ) ) )
136 119 131 135 3eqtrd ⊢ ( 𝜑 → ( 𝑈 ‘ ( ◡ 𝑊 ‘ 𝐽 ) ) = ( ( 𝑊 prefix 𝐸 ) ‘ ( ◡ 𝑊 ‘ 𝐽 ) ) )
137 pfxfv ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 𝐸 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( ◡ 𝑊 ‘ 𝐽 ) ∈ ( 0 ..^ 𝐸 ) ) → ( ( 𝑊 prefix 𝐸 ) ‘ ( ◡ 𝑊 ‘ 𝐽 ) ) = ( 𝑊 ‘ ( ◡ 𝑊 ‘ 𝐽 ) ) )
138 20 86 126 137 syl3anc ⊢ ( 𝜑 → ( ( 𝑊 prefix 𝐸 ) ‘ ( ◡ 𝑊 ‘ 𝐽 ) ) = ( 𝑊 ‘ ( ◡ 𝑊 ‘ 𝐽 ) ) )
139 f1f1orn ⊢ ( 𝑊 : dom 𝑊 –1-1→ 𝐷 → 𝑊 : dom 𝑊 –1-1-onto→ ran 𝑊 )
140 27 139 syl ⊢ ( 𝜑 → 𝑊 : dom 𝑊 –1-1-onto→ ran 𝑊 )
141 f1ocnvfv2 ⊢ ( ( 𝑊 : dom 𝑊 –1-1-onto→ ran 𝑊 ∧ 𝐽 ∈ ran 𝑊 ) → ( 𝑊 ‘ ( ◡ 𝑊 ‘ 𝐽 ) ) = 𝐽 )
142 140 6 141 syl2anc ⊢ ( 𝜑 → ( 𝑊 ‘ ( ◡ 𝑊 ‘ 𝐽 ) ) = 𝐽 )
143 136 138 142 3eqtrd ⊢ ( 𝜑 → ( 𝑈 ‘ ( ◡ 𝑊 ‘ 𝐽 ) ) = 𝐽 )
144 143 fveq2d ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑈 ) ‘ ( 𝑈 ‘ ( ◡ 𝑊 ‘ 𝐽 ) ) ) = ( ( 𝑀 ‘ 𝑈 ) ‘ 𝐽 ) )
145 55 118 144 3eqtr2d ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑊 ) ‘ ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝐽 ) ) = ( ( 𝑀 ‘ 𝑈 ) ‘ 𝐽 ) )
146 145 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 = 𝐽 ) → ( ( 𝑀 ‘ 𝑊 ) ‘ ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝐽 ) ) = ( ( 𝑀 ‘ 𝑈 ) ‘ 𝐽 ) )
147 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 = 𝐽 ) → 𝑖 = 𝐽 )
148 147 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 = 𝐽 ) → ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝑖 ) = ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝐽 ) )
149 148 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 = 𝐽 ) → ( ( 𝑀 ‘ 𝑊 ) ‘ ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝑖 ) ) = ( ( 𝑀 ‘ 𝑊 ) ‘ ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝐽 ) ) )
150 147 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 = 𝐽 ) → ( ( 𝑀 ‘ 𝑈 ) ‘ 𝑖 ) = ( ( 𝑀 ‘ 𝑈 ) ‘ 𝐽 ) )
151 146 149 150 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 = 𝐽 ) → ( ( 𝑀 ‘ 𝑊 ) ‘ ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝑖 ) ) = ( ( 𝑀 ‘ 𝑈 ) ‘ 𝑖 ) )
152 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) → 𝐷 ∈ 𝑉 )
153 18 31 s2cld ⊢ ( 𝜑 → ⟨“ 𝐼 𝐽 ”⟩ ∈ Word 𝐷 )
154 153 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) → ⟨“ 𝐼 𝐽 ”⟩ ∈ Word 𝐷 )
155 18 31 35 s2f1 ⊢ ( 𝜑 → ⟨“ 𝐼 𝐽 ”⟩ : dom ⟨“ 𝐼 𝐽 ”⟩ –1-1→ 𝐷 )
156 155 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) → ⟨“ 𝐼 𝐽 ”⟩ : dom ⟨“ 𝐼 𝐽 ”⟩ –1-1→ 𝐷 )
157 30 sselda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) → 𝑖 ∈ 𝐷 )
158 157 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) → 𝑖 ∈ 𝐷 )
159 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) → 𝑖 ∈ ran 𝑊 )
160 32 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) → ¬ 𝐼 ∈ ran 𝑊 )
161 nelne2 ⊢ ( ( 𝑖 ∈ ran 𝑊 ∧ ¬ 𝐼 ∈ ran 𝑊 ) → 𝑖 ≠ 𝐼 )
162 159 160 161 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) → 𝑖 ≠ 𝐼 )
163 162 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) → 𝑖 ≠ 𝐼 )
164 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) → 𝑖 ≠ 𝐽 )
165 163 164 nelprd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) → ¬ 𝑖 ∈ { 𝐼 , 𝐽 } )
166 18 31 s2rn ⊢ ( 𝜑 → ran ⟨“ 𝐼 𝐽 ”⟩ = { 𝐼 , 𝐽 } )
167 166 eleq2d ⊢ ( 𝜑 → ( 𝑖 ∈ ran ⟨“ 𝐼 𝐽 ”⟩ ↔ 𝑖 ∈ { 𝐼 , 𝐽 } ) )
168 167 notbid ⊢ ( 𝜑 → ( ¬ 𝑖 ∈ ran ⟨“ 𝐼 𝐽 ”⟩ ↔ ¬ 𝑖 ∈ { 𝐼 , 𝐽 } ) )
169 168 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) → ( ¬ 𝑖 ∈ ran ⟨“ 𝐼 𝐽 ”⟩ ↔ ¬ 𝑖 ∈ { 𝐼 , 𝐽 } ) )
170 165 169 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) → ¬ 𝑖 ∈ ran ⟨“ 𝐼 𝐽 ”⟩ )
171 1 152 154 156 158 170 cycpmfv3 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) → ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝑖 ) = 𝑖 )
172 171 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) → ( ( 𝑀 ‘ 𝑊 ) ‘ ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝑖 ) ) = ( ( 𝑀 ‘ 𝑊 ) ‘ 𝑖 ) )
173 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) ∧ ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 0 ..^ 𝐸 ) ) → 𝐷 ∈ 𝑉 )
174 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) ∧ ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 0 ..^ 𝐸 ) ) → 𝑊 ∈ dom 𝑀 )
175 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) ∧ ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 0 ..^ 𝐸 ) ) → 𝐼 ∈ ( 𝐷 ∖ ran 𝑊 ) )
176 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) ∧ ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 0 ..^ 𝐸 ) ) → 𝐽 ∈ ran 𝑊 )
177 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) ∧ ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 0 ..^ 𝐸 ) ) → 𝑖 ∈ ran 𝑊 )
178 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) ∧ ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 0 ..^ 𝐸 ) ) → 𝑖 ≠ 𝐽 )
179 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) ∧ ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 0 ..^ 𝐸 ) ) → ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 0 ..^ 𝐸 ) )
180 1 2 173 174 175 176 7 8 177 178 179 cycpmco2lem7 ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) ∧ ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 0 ..^ 𝐸 ) ) → ( ( 𝑀 ‘ 𝑈 ) ‘ 𝑖 ) = ( ( 𝑀 ‘ 𝑊 ) ‘ 𝑖 ) )
181 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) ∧ ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 𝐸 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) → 𝐷 ∈ 𝑉 )
182 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) ∧ ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 𝐸 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) → 𝑊 ∈ dom 𝑀 )
183 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) ∧ ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 𝐸 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) → 𝐼 ∈ ( 𝐷 ∖ ran 𝑊 ) )
184 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) ∧ ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 𝐸 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) → 𝐽 ∈ ran 𝑊 )
185 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) ∧ ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 𝐸 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) → 𝑖 ∈ ran 𝑊 )
186 162 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) ∧ ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 𝐸 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) → 𝑖 ≠ 𝐼 )
187 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) ∧ ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 𝐸 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) → ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 𝐸 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) )
188 1 2 181 182 183 184 7 8 185 186 187 cycpmco2lem6 ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) ∧ ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 𝐸 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) → ( ( 𝑀 ‘ 𝑈 ) ‘ 𝑖 ) = ( ( 𝑀 ‘ 𝑊 ) ‘ 𝑖 ) )
189 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) ∧ ( ◡ 𝑈 ‘ 𝑖 ) = ( ( ♯ ‘ 𝑈 ) − 1 ) ) → 𝐷 ∈ 𝑉 )
190 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) ∧ ( ◡ 𝑈 ‘ 𝑖 ) = ( ( ♯ ‘ 𝑈 ) − 1 ) ) → 𝑊 ∈ dom 𝑀 )
191 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) ∧ ( ◡ 𝑈 ‘ 𝑖 ) = ( ( ♯ ‘ 𝑈 ) − 1 ) ) → 𝐼 ∈ ( 𝐷 ∖ ran 𝑊 ) )
192 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) ∧ ( ◡ 𝑈 ‘ 𝑖 ) = ( ( ♯ ‘ 𝑈 ) − 1 ) ) → 𝐽 ∈ ran 𝑊 )
193 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) ∧ ( ◡ 𝑈 ‘ 𝑖 ) = ( ( ♯ ‘ 𝑈 ) − 1 ) ) → 𝑖 ∈ ran 𝑊 )
194 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) ∧ ( ◡ 𝑈 ‘ 𝑖 ) = ( ( ♯ ‘ 𝑈 ) − 1 ) ) → ( ◡ 𝑈 ‘ 𝑖 ) = ( ( ♯ ‘ 𝑈 ) − 1 ) )
195 1 2 189 190 191 192 7 8 193 194 cycpmco2lem5 ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) ∧ ( ◡ 𝑈 ‘ 𝑖 ) = ( ( ♯ ‘ 𝑈 ) − 1 ) ) → ( ( 𝑀 ‘ 𝑈 ) ‘ 𝑖 ) = ( ( 𝑀 ‘ 𝑊 ) ‘ 𝑖 ) )
196 f1f1orn ⊢ ( 𝑈 : dom 𝑈 –1-1→ 𝐷 → 𝑈 : dom 𝑈 –1-1-onto→ ran 𝑈 )
197 47 196 syl ⊢ ( 𝜑 → 𝑈 : dom 𝑈 –1-1-onto→ ran 𝑈 )
198 ssun1 ⊢ ran 𝑊 ⊆ ( ran 𝑊 ∪ { 𝐼 } )
199 1 2 3 4 5 6 7 8 cycpmco2rn ⊢ ( 𝜑 → ran 𝑈 = ( ran 𝑊 ∪ { 𝐼 } ) )
200 198 199 sseqtrrid ⊢ ( 𝜑 → ran 𝑊 ⊆ ran 𝑈 )
201 200 sselda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) → 𝑖 ∈ ran 𝑈 )
202 f1ocnvdm ⊢ ( ( 𝑈 : dom 𝑈 –1-1-onto→ ran 𝑈 ∧ 𝑖 ∈ ran 𝑈 ) → ( ◡ 𝑈 ‘ 𝑖 ) ∈ dom 𝑈 )
203 197 201 202 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) → ( ◡ 𝑈 ‘ 𝑖 ) ∈ dom 𝑈 )
204 wrddm ⊢ ( 𝑈 ∈ Word 𝐷 → dom 𝑈 = ( 0 ..^ ( ♯ ‘ 𝑈 ) ) )
205 46 204 syl ⊢ ( 𝜑 → dom 𝑈 = ( 0 ..^ ( ♯ ‘ 𝑈 ) ) )
206 205 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) → dom 𝑈 = ( 0 ..^ ( ♯ ‘ 𝑈 ) ) )
207 203 206 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) → ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑈 ) ) )
208 65 nn0zd ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℤ )
209 208 peano2zd ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑊 ) + 1 ) ∈ ℤ )
210 110 209 eqeltrd ⊢ ( 𝜑 → ( ♯ ‘ 𝑈 ) ∈ ℤ )
211 fzoval ⊢ ( ( ♯ ‘ 𝑈 ) ∈ ℤ → ( 0 ..^ ( ♯ ‘ 𝑈 ) ) = ( 0 ... ( ( ♯ ‘ 𝑈 ) − 1 ) ) )
212 210 211 syl ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝑈 ) ) = ( 0 ... ( ( ♯ ‘ 𝑈 ) − 1 ) ) )
213 212 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) → ( 0 ..^ ( ♯ ‘ 𝑈 ) ) = ( 0 ... ( ( ♯ ‘ 𝑈 ) − 1 ) ) )
214 207 213 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) → ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 0 ... ( ( ♯ ‘ 𝑈 ) − 1 ) ) )
215 elfzr ⊢ ( ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 0 ... ( ( ♯ ‘ 𝑈 ) − 1 ) ) → ( ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ∨ ( ◡ 𝑈 ‘ 𝑖 ) = ( ( ♯ ‘ 𝑈 ) − 1 ) ) )
216 214 215 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) → ( ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ∨ ( ◡ 𝑈 ‘ 𝑖 ) = ( ( ♯ ‘ 𝑈 ) − 1 ) ) )
217 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) → ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) )
218 99 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) → 𝐸 ∈ ℤ )
219 fzospliti ⊢ ( ( ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ∧ 𝐸 ∈ ℤ ) → ( ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 0 ..^ 𝐸 ) ∨ ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 𝐸 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) )
220 217 218 219 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) → ( ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 0 ..^ 𝐸 ) ∨ ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 𝐸 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) )
221 220 ex ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) → ( ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) → ( ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 0 ..^ 𝐸 ) ∨ ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 𝐸 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) ) )
222 221 orim1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) → ( ( ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ∨ ( ◡ 𝑈 ‘ 𝑖 ) = ( ( ♯ ‘ 𝑈 ) − 1 ) ) → ( ( ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 0 ..^ 𝐸 ) ∨ ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 𝐸 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) ∨ ( ◡ 𝑈 ‘ 𝑖 ) = ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) )
223 216 222 mpd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) → ( ( ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 0 ..^ 𝐸 ) ∨ ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 𝐸 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) ∨ ( ◡ 𝑈 ‘ 𝑖 ) = ( ( ♯ ‘ 𝑈 ) − 1 ) ) )
224 df-3or ⊢ ( ( ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 0 ..^ 𝐸 ) ∨ ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 𝐸 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ∨ ( ◡ 𝑈 ‘ 𝑖 ) = ( ( ♯ ‘ 𝑈 ) − 1 ) ) ↔ ( ( ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 0 ..^ 𝐸 ) ∨ ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 𝐸 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) ∨ ( ◡ 𝑈 ‘ 𝑖 ) = ( ( ♯ ‘ 𝑈 ) − 1 ) ) )
225 223 224 sylibr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) → ( ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 0 ..^ 𝐸 ) ∨ ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 𝐸 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ∨ ( ◡ 𝑈 ‘ 𝑖 ) = ( ( ♯ ‘ 𝑈 ) − 1 ) ) )
226 225 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) → ( ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 0 ..^ 𝐸 ) ∨ ( ◡ 𝑈 ‘ 𝑖 ) ∈ ( 𝐸 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ∨ ( ◡ 𝑈 ‘ 𝑖 ) = ( ( ♯ ‘ 𝑈 ) − 1 ) ) )
227 180 188 195 226 mpjao3dan ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) → ( ( 𝑀 ‘ 𝑈 ) ‘ 𝑖 ) = ( ( 𝑀 ‘ 𝑊 ) ‘ 𝑖 ) )
228 172 227 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) ∧ 𝑖 ≠ 𝐽 ) → ( ( 𝑀 ‘ 𝑊 ) ‘ ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝑖 ) ) = ( ( 𝑀 ‘ 𝑈 ) ‘ 𝑖 ) )
229 151 228 pm2.61dane ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ran 𝑊 ) → ( ( 𝑀 ‘ 𝑊 ) ‘ ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝑖 ) ) = ( ( 𝑀 ‘ 𝑈 ) ‘ 𝑖 ) )
230 229 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐷 ) ∧ 𝑖 ∈ ran 𝑊 ) → ( ( 𝑀 ‘ 𝑊 ) ‘ ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝑖 ) ) = ( ( 𝑀 ‘ 𝑈 ) ‘ 𝑖 ) )
231 1 2 3 4 5 6 7 8 cycpmco2lem4 ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑊 ) ‘ ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝐼 ) ) = ( ( 𝑀 ‘ 𝑈 ) ‘ 𝐼 ) )
232 231 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) ) ∧ 𝑖 = 𝐼 ) → ( ( 𝑀 ‘ 𝑊 ) ‘ ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝐼 ) ) = ( ( 𝑀 ‘ 𝑈 ) ‘ 𝐼 ) )
233 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) ) ∧ 𝑖 = 𝐼 ) → 𝑖 = 𝐼 )
234 233 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) ) ∧ 𝑖 = 𝐼 ) → ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝑖 ) = ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝐼 ) )
235 234 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) ) ∧ 𝑖 = 𝐼 ) → ( ( 𝑀 ‘ 𝑊 ) ‘ ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝑖 ) ) = ( ( 𝑀 ‘ 𝑊 ) ‘ ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝐼 ) ) )
236 233 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) ) ∧ 𝑖 = 𝐼 ) → ( ( 𝑀 ‘ 𝑈 ) ‘ 𝑖 ) = ( ( 𝑀 ‘ 𝑈 ) ‘ 𝐼 ) )
237 232 235 236 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) ) ∧ 𝑖 = 𝐼 ) → ( ( 𝑀 ‘ 𝑊 ) ‘ ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝑖 ) ) = ( ( 𝑀 ‘ 𝑈 ) ‘ 𝑖 ) )
238 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) ) ∧ 𝑖 ≠ 𝐼 ) → 𝐷 ∈ 𝑉 )
239 20 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) ) ∧ 𝑖 ≠ 𝐼 ) → 𝑊 ∈ Word 𝐷 )
240 27 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) ) ∧ 𝑖 ≠ 𝐼 ) → 𝑊 : dom 𝑊 –1-1→ 𝐷 )
241 simplr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) ) ∧ 𝑖 ≠ 𝐼 ) → 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) )
242 241 eldifad ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) ) ∧ 𝑖 ≠ 𝐼 ) → 𝑖 ∈ 𝐷 )
243 241 eldifbd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) ) ∧ 𝑖 ≠ 𝐼 ) → ¬ 𝑖 ∈ ran 𝑊 )
244 1 238 239 240 242 243 cycpmfv3 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) ) ∧ 𝑖 ≠ 𝐼 ) → ( ( 𝑀 ‘ 𝑊 ) ‘ 𝑖 ) = 𝑖 )
245 153 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) ) ∧ 𝑖 ≠ 𝐼 ) → ⟨“ 𝐼 𝐽 ”⟩ ∈ Word 𝐷 )
246 155 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) ) ∧ 𝑖 ≠ 𝐼 ) → ⟨“ 𝐼 𝐽 ”⟩ : dom ⟨“ 𝐼 𝐽 ”⟩ –1-1→ 𝐷 )
247 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) ) ∧ 𝑖 ≠ 𝐼 ) → 𝑖 ≠ 𝐼 )
248 eldifn ⊢ ( 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) → ¬ 𝑖 ∈ ran 𝑊 )
249 nelne2 ⊢ ( ( 𝐽 ∈ ran 𝑊 ∧ ¬ 𝑖 ∈ ran 𝑊 ) → 𝐽 ≠ 𝑖 )
250 6 248 249 syl2an ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) ) → 𝐽 ≠ 𝑖 )
251 250 necomd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) ) → 𝑖 ≠ 𝐽 )
252 251 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) ) ∧ 𝑖 ≠ 𝐼 ) → 𝑖 ≠ 𝐽 )
253 247 252 nelprd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) ) ∧ 𝑖 ≠ 𝐼 ) → ¬ 𝑖 ∈ { 𝐼 , 𝐽 } )
254 168 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) ) ∧ 𝑖 ≠ 𝐼 ) → ( ¬ 𝑖 ∈ ran ⟨“ 𝐼 𝐽 ”⟩ ↔ ¬ 𝑖 ∈ { 𝐼 , 𝐽 } ) )
255 253 254 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) ) ∧ 𝑖 ≠ 𝐼 ) → ¬ 𝑖 ∈ ran ⟨“ 𝐼 𝐽 ”⟩ )
256 1 238 245 246 242 255 cycpmfv3 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) ) ∧ 𝑖 ≠ 𝐼 ) → ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝑖 ) = 𝑖 )
257 256 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) ) ∧ 𝑖 ≠ 𝐼 ) → ( ( 𝑀 ‘ 𝑊 ) ‘ ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝑖 ) ) = ( ( 𝑀 ‘ 𝑊 ) ‘ 𝑖 ) )
258 46 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) ) ∧ 𝑖 ≠ 𝐼 ) → 𝑈 ∈ Word 𝐷 )
259 47 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) ) ∧ 𝑖 ≠ 𝐼 ) → 𝑈 : dom 𝑈 –1-1→ 𝐷 )
260 199 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) ) ∧ 𝑖 ≠ 𝐼 ) → ran 𝑈 = ( ran 𝑊 ∪ { 𝐼 } ) )
261 nelsn ⊢ ( 𝑖 ≠ 𝐼 → ¬ 𝑖 ∈ { 𝐼 } )
262 261 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) ) ∧ 𝑖 ≠ 𝐼 ) → ¬ 𝑖 ∈ { 𝐼 } )
263 nelun ⊢ ( ran 𝑈 = ( ran 𝑊 ∪ { 𝐼 } ) → ( ¬ 𝑖 ∈ ran 𝑈 ↔ ( ¬ 𝑖 ∈ ran 𝑊 ∧ ¬ 𝑖 ∈ { 𝐼 } ) ) )
264 263 biimpar ⊢ ( ( ran 𝑈 = ( ran 𝑊 ∪ { 𝐼 } ) ∧ ( ¬ 𝑖 ∈ ran 𝑊 ∧ ¬ 𝑖 ∈ { 𝐼 } ) ) → ¬ 𝑖 ∈ ran 𝑈 )
265 260 243 262 264 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) ) ∧ 𝑖 ≠ 𝐼 ) → ¬ 𝑖 ∈ ran 𝑈 )
266 1 238 258 259 242 265 cycpmfv3 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) ) ∧ 𝑖 ≠ 𝐼 ) → ( ( 𝑀 ‘ 𝑈 ) ‘ 𝑖 ) = 𝑖 )
267 244 257 266 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) ) ∧ 𝑖 ≠ 𝐼 ) → ( ( 𝑀 ‘ 𝑊 ) ‘ ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝑖 ) ) = ( ( 𝑀 ‘ 𝑈 ) ‘ 𝑖 ) )
268 237 267 pm2.61dane ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) ) → ( ( 𝑀 ‘ 𝑊 ) ‘ ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝑖 ) ) = ( ( 𝑀 ‘ 𝑈 ) ‘ 𝑖 ) )
269 268 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐷 ) ∧ 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) ) → ( ( 𝑀 ‘ 𝑊 ) ‘ ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝑖 ) ) = ( ( 𝑀 ‘ 𝑈 ) ‘ 𝑖 ) )
270 undif ⊢ ( ran 𝑊 ⊆ 𝐷 ↔ ( ran 𝑊 ∪ ( 𝐷 ∖ ran 𝑊 ) ) = 𝐷 )
271 30 270 sylib ⊢ ( 𝜑 → ( ran 𝑊 ∪ ( 𝐷 ∖ ran 𝑊 ) ) = 𝐷 )
272 271 eleq2d ⊢ ( 𝜑 → ( 𝑖 ∈ ( ran 𝑊 ∪ ( 𝐷 ∖ ran 𝑊 ) ) ↔ 𝑖 ∈ 𝐷 ) )
273 elun ⊢ ( 𝑖 ∈ ( ran 𝑊 ∪ ( 𝐷 ∖ ran 𝑊 ) ) ↔ ( 𝑖 ∈ ran 𝑊 ∨ 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) ) )
274 272 273 bitr3di ⊢ ( 𝜑 → ( 𝑖 ∈ 𝐷 ↔ ( 𝑖 ∈ ran 𝑊 ∨ 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) ) ) )
275 274 biimpa ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐷 ) → ( 𝑖 ∈ ran 𝑊 ∨ 𝑖 ∈ ( 𝐷 ∖ ran 𝑊 ) ) )
276 230 269 275 mpjaodan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐷 ) → ( ( 𝑀 ‘ 𝑊 ) ‘ ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝑖 ) ) = ( ( 𝑀 ‘ 𝑈 ) ‘ 𝑖 ) )
277 53 276 eqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐷 ) → ( ( ( 𝑀 ‘ 𝑊 ) ∘ ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ) ‘ 𝑖 ) = ( ( 𝑀 ‘ 𝑈 ) ‘ 𝑖 ) )
278 42 51 277 eqfnfvd ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑊 ) ∘ ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ) = ( 𝑀 ‘ 𝑈 ) )