Metamath Proof Explorer

Theorem efgredlemd

Description: The reduced word that forms the base of the sequence in efgsval is uniquely determined, given the ending representation. (Contributed by Mario Carneiro, 1-Oct-2015) (Proof shortened by AV, 15-Oct-2022)

Ref Expression
Hypotheses efgval.w ⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
efgval.r ⊢ ∼ = ( ~FG ‘ 𝐼 )
efgval2.m ⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ )
efgval2.t ⊢ 𝑇 = ( 𝑣 ∈ 𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) ) )
efgred.d ⊢ 𝐷 = ( 𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) )
efgred.s ⊢ 𝑆 = ( 𝑚 ∈ { 𝑡 ∈ ( Word 𝑊 ∖ { ∅ } ) ∣ ( ( 𝑡 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) } ↦ ( 𝑚 ‘ ( ( ♯ ‘ 𝑚 ) − 1 ) ) )
efgredlem.1 ⊢ ( 𝜑 → ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) )
efgredlem.2 ⊢ ( 𝜑 → 𝐴 ∈ dom 𝑆 )
efgredlem.3 ⊢ ( 𝜑 → 𝐵 ∈ dom 𝑆 )
efgredlem.4 ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐴 ) = ( 𝑆 ‘ 𝐵 ) )
efgredlem.5 ⊢ ( 𝜑 → ¬ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) )
efgredlemb.k ⊢ 𝐾 = ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 )
efgredlemb.l ⊢ 𝐿 = ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 )
efgredlemb.p ⊢ ( 𝜑 → 𝑃 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ) )
efgredlemb.q ⊢ ( 𝜑 → 𝑄 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ) )
efgredlemb.u ⊢ ( 𝜑 → 𝑈 ∈ ( 𝐼 × 2o ) )
efgredlemb.v ⊢ ( 𝜑 → 𝑉 ∈ ( 𝐼 × 2o ) )
efgredlemb.6 ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐴 ) = ( 𝑃 ( 𝑇 ‘ ( 𝐴 ‘ 𝐾 ) ) 𝑈 ) )
efgredlemb.7 ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐵 ) = ( 𝑄 ( 𝑇 ‘ ( 𝐵 ‘ 𝐿 ) ) 𝑉 ) )
efgredlemb.8 ⊢ ( 𝜑 → ¬ ( 𝐴 ‘ 𝐾 ) = ( 𝐵 ‘ 𝐿 ) )
efgredlemd.9 ⊢ ( 𝜑 → 𝑃 ∈ ( ℤ≥ ‘ ( 𝑄 + 2 ) ) )
efgredlemd.c ⊢ ( 𝜑 → 𝐶 ∈ dom 𝑆 )
efgredlemd.sc ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐶 ) = ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ ( 𝑄 + 2 ) , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) )
Assertion efgredlemd ( 𝜑 → ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) )

Proof

Step Hyp Ref Expression
1 efgval.w ⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
2 efgval.r ⊢ ∼ = ( ~FG ‘ 𝐼 )
3 efgval2.m ⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ )
4 efgval2.t ⊢ 𝑇 = ( 𝑣 ∈ 𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) ) )
5 efgred.d ⊢ 𝐷 = ( 𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) )
6 efgred.s ⊢ 𝑆 = ( 𝑚 ∈ { 𝑡 ∈ ( Word 𝑊 ∖ { ∅ } ) ∣ ( ( 𝑡 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) } ↦ ( 𝑚 ‘ ( ( ♯ ‘ 𝑚 ) − 1 ) ) )
7 efgredlem.1 ⊢ ( 𝜑 → ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) )
8 efgredlem.2 ⊢ ( 𝜑 → 𝐴 ∈ dom 𝑆 )
9 efgredlem.3 ⊢ ( 𝜑 → 𝐵 ∈ dom 𝑆 )
10 efgredlem.4 ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐴 ) = ( 𝑆 ‘ 𝐵 ) )
11 efgredlem.5 ⊢ ( 𝜑 → ¬ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) )
12 efgredlemb.k ⊢ 𝐾 = ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 )
13 efgredlemb.l ⊢ 𝐿 = ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 )
14 efgredlemb.p ⊢ ( 𝜑 → 𝑃 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ) )
15 efgredlemb.q ⊢ ( 𝜑 → 𝑄 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ) )
16 efgredlemb.u ⊢ ( 𝜑 → 𝑈 ∈ ( 𝐼 × 2o ) )
17 efgredlemb.v ⊢ ( 𝜑 → 𝑉 ∈ ( 𝐼 × 2o ) )
18 efgredlemb.6 ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐴 ) = ( 𝑃 ( 𝑇 ‘ ( 𝐴 ‘ 𝐾 ) ) 𝑈 ) )
19 efgredlemb.7 ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐵 ) = ( 𝑄 ( 𝑇 ‘ ( 𝐵 ‘ 𝐿 ) ) 𝑉 ) )
20 efgredlemb.8 ⊢ ( 𝜑 → ¬ ( 𝐴 ‘ 𝐾 ) = ( 𝐵 ‘ 𝐿 ) )
21 efgredlemd.9 ⊢ ( 𝜑 → 𝑃 ∈ ( ℤ≥ ‘ ( 𝑄 + 2 ) ) )
22 efgredlemd.c ⊢ ( 𝜑 → 𝐶 ∈ dom 𝑆 )
23 efgredlemd.sc ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐶 ) = ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ ( 𝑄 + 2 ) , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) )
24 1 2 3 4 5 6 efgsdm ⊢ ( 𝐶 ∈ dom 𝑆 ↔ ( 𝐶 ∈ ( Word 𝑊 ∖ { ∅ } ) ∧ ( 𝐶 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝐶 ) ) ( 𝐶 ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( 𝐶 ‘ ( 𝑖 − 1 ) ) ) ) )
25 24 simp1bi ⊢ ( 𝐶 ∈ dom 𝑆 → 𝐶 ∈ ( Word 𝑊 ∖ { ∅ } ) )
26 22 25 syl ⊢ ( 𝜑 → 𝐶 ∈ ( Word 𝑊 ∖ { ∅ } ) )
27 26 eldifad ⊢ ( 𝜑 → 𝐶 ∈ Word 𝑊 )
28 1 2 3 4 5 6 efgsdm ⊢ ( 𝐴 ∈ dom 𝑆 ↔ ( 𝐴 ∈ ( Word 𝑊 ∖ { ∅ } ) ∧ ( 𝐴 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝐴 ) ) ( 𝐴 ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( 𝐴 ‘ ( 𝑖 − 1 ) ) ) ) )
29 28 simp1bi ⊢ ( 𝐴 ∈ dom 𝑆 → 𝐴 ∈ ( Word 𝑊 ∖ { ∅ } ) )
30 8 29 syl ⊢ ( 𝜑 → 𝐴 ∈ ( Word 𝑊 ∖ { ∅ } ) )
31 30 eldifad ⊢ ( 𝜑 → 𝐴 ∈ Word 𝑊 )
32 wrdf ⊢ ( 𝐴 ∈ Word 𝑊 → 𝐴 : ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ⟶ 𝑊 )
33 31 32 syl ⊢ ( 𝜑 → 𝐴 : ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ⟶ 𝑊 )
34 fzossfz ⊢ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ⊆ ( 0 ... ( ( ♯ ‘ 𝐴 ) − 1 ) )
35 lencl ⊢ ( 𝐴 ∈ Word 𝑊 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
36 31 35 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
37 36 nn0zd ⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ℤ )
38 fzoval ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℤ → ( 0 ..^ ( ♯ ‘ 𝐴 ) ) = ( 0 ... ( ( ♯ ‘ 𝐴 ) − 1 ) ) )
39 37 38 syl ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐴 ) ) = ( 0 ... ( ( ♯ ‘ 𝐴 ) − 1 ) ) )
40 34 39 sseqtrrid ⊢ ( 𝜑 → ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) )
41 1 2 3 4 5 6 7 8 9 10 11 efgredlema ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ℕ ∧ ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ℕ ) )
42 41 simpld ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ℕ )
43 fzo0end ⊢ ( ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ℕ → ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) )
44 42 43 syl ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) )
45 12 44 eqeltrid ⊢ ( 𝜑 → 𝐾 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) )
46 40 45 sseldd ⊢ ( 𝜑 → 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) )
47 33 46 ffvelrnd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐾 ) ∈ 𝑊 )
48 47 s1cld ⊢ ( 𝜑 → ⟨“ ( 𝐴 ‘ 𝐾 ) ”⟩ ∈ Word 𝑊 )
49 eldifsn ⊢ ( 𝐶 ∈ ( Word 𝑊 ∖ { ∅ } ) ↔ ( 𝐶 ∈ Word 𝑊 ∧ 𝐶 ≠ ∅ ) )
50 lennncl ⊢ ( ( 𝐶 ∈ Word 𝑊 ∧ 𝐶 ≠ ∅ ) → ( ♯ ‘ 𝐶 ) ∈ ℕ )
51 49 50 sylbi ⊢ ( 𝐶 ∈ ( Word 𝑊 ∖ { ∅ } ) → ( ♯ ‘ 𝐶 ) ∈ ℕ )
52 26 51 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐶 ) ∈ ℕ )
53 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ↔ ( ♯ ‘ 𝐶 ) ∈ ℕ )
54 52 53 sylibr ⊢ ( 𝜑 → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) )
55 ccatval1 ⊢ ( ( 𝐶 ∈ Word 𝑊 ∧ ⟨“ ( 𝐴 ‘ 𝐾 ) ”⟩ ∈ Word 𝑊 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) → ( ( 𝐶 ++ ⟨“ ( 𝐴 ‘ 𝐾 ) ”⟩ ) ‘ 0 ) = ( 𝐶 ‘ 0 ) )
56 27 48 54 55 syl3anc ⊢ ( 𝜑 → ( ( 𝐶 ++ ⟨“ ( 𝐴 ‘ 𝐾 ) ”⟩ ) ‘ 0 ) = ( 𝐶 ‘ 0 ) )
57 1 2 3 4 5 6 efgsdm ⊢ ( 𝐵 ∈ dom 𝑆 ↔ ( 𝐵 ∈ ( Word 𝑊 ∖ { ∅ } ) ∧ ( 𝐵 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝐵 ) ) ( 𝐵 ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( 𝐵 ‘ ( 𝑖 − 1 ) ) ) ) )
58 57 simp1bi ⊢ ( 𝐵 ∈ dom 𝑆 → 𝐵 ∈ ( Word 𝑊 ∖ { ∅ } ) )
59 9 58 syl ⊢ ( 𝜑 → 𝐵 ∈ ( Word 𝑊 ∖ { ∅ } ) )
60 59 eldifad ⊢ ( 𝜑 → 𝐵 ∈ Word 𝑊 )
61 wrdf ⊢ ( 𝐵 ∈ Word 𝑊 → 𝐵 : ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ⟶ 𝑊 )
62 60 61 syl ⊢ ( 𝜑 → 𝐵 : ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ⟶ 𝑊 )
63 fzossfz ⊢ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ⊆ ( 0 ... ( ( ♯ ‘ 𝐵 ) − 1 ) )
64 lencl ⊢ ( 𝐵 ∈ Word 𝑊 → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
65 60 64 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
66 65 nn0zd ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℤ )
67 fzoval ⊢ ( ( ♯ ‘ 𝐵 ) ∈ ℤ → ( 0 ..^ ( ♯ ‘ 𝐵 ) ) = ( 0 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) )
68 66 67 syl ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐵 ) ) = ( 0 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) )
69 63 68 sseqtrrid ⊢ ( 𝜑 → ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) )
70 41 simprd ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ℕ )
71 fzo0end ⊢ ( ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ℕ → ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) )
72 70 71 syl ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) )
73 13 72 eqeltrid ⊢ ( 𝜑 → 𝐿 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) )
74 69 73 sseldd ⊢ ( 𝜑 → 𝐿 ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) )
75 62 74 ffvelrnd ⊢ ( 𝜑 → ( 𝐵 ‘ 𝐿 ) ∈ 𝑊 )
76 75 s1cld ⊢ ( 𝜑 → ⟨“ ( 𝐵 ‘ 𝐿 ) ”⟩ ∈ Word 𝑊 )
77 ccatval1 ⊢ ( ( 𝐶 ∈ Word 𝑊 ∧ ⟨“ ( 𝐵 ‘ 𝐿 ) ”⟩ ∈ Word 𝑊 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) → ( ( 𝐶 ++ ⟨“ ( 𝐵 ‘ 𝐿 ) ”⟩ ) ‘ 0 ) = ( 𝐶 ‘ 0 ) )
78 27 76 54 77 syl3anc ⊢ ( 𝜑 → ( ( 𝐶 ++ ⟨“ ( 𝐵 ‘ 𝐿 ) ”⟩ ) ‘ 0 ) = ( 𝐶 ‘ 0 ) )
79 56 78 eqtr4d ⊢ ( 𝜑 → ( ( 𝐶 ++ ⟨“ ( 𝐴 ‘ 𝐾 ) ”⟩ ) ‘ 0 ) = ( ( 𝐶 ++ ⟨“ ( 𝐵 ‘ 𝐿 ) ”⟩ ) ‘ 0 ) )
80 fviss ⊢ ( I ‘ Word ( 𝐼 × 2o ) ) ⊆ Word ( 𝐼 × 2o )
81 1 80 eqsstri ⊢ 𝑊 ⊆ Word ( 𝐼 × 2o )
82 81 47 sseldi ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐾 ) ∈ Word ( 𝐼 × 2o ) )
83 lencl ⊢ ( ( 𝐴 ‘ 𝐾 ) ∈ Word ( 𝐼 × 2o ) → ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ∈ ℕ0 )
84 82 83 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ∈ ℕ0 )
85 84 nn0red ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ∈ ℝ )
86 2rp ⊢ 2 ∈ ℝ+
87 ltaddrp ⊢ ( ( ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ∈ ℝ ∧ 2 ∈ ℝ+ ) → ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) < ( ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) + 2 ) )
88 85 86 87 sylancl ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) < ( ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) + 2 ) )
89 36 nn0red ⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ℝ )
90 89 lem1d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) − 1 ) ≤ ( ♯ ‘ 𝐴 ) )
91 fznn ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℤ → ( ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ↔ ( ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ℕ ∧ ( ( ♯ ‘ 𝐴 ) − 1 ) ≤ ( ♯ ‘ 𝐴 ) ) ) )
92 37 91 syl ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ↔ ( ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ℕ ∧ ( ( ♯ ‘ 𝐴 ) − 1 ) ≤ ( ♯ ‘ 𝐴 ) ) ) )
93 42 90 92 mpbir2and ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) )
94 1 2 3 4 5 6 efgsres ⊢ ( ( 𝐴 ∈ dom 𝑆 ∧ ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ∈ dom 𝑆 )
95 8 93 94 syl2anc ⊢ ( 𝜑 → ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ∈ dom 𝑆 )
96 1 2 3 4 5 6 efgsval ⊢ ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ∈ dom 𝑆 → ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) = ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ ( ( ♯ ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) − 1 ) ) )
97 95 96 syl ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) = ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ ( ( ♯ ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) − 1 ) ) )
98 fz1ssfz0 ⊢ ( 1 ... ( ♯ ‘ 𝐴 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝐴 ) )
99 98 93 sseldi ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) )
100 pfxres ⊢ ( ( 𝐴 ∈ Word 𝑊 ∧ ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐴 prefix ( ( ♯ ‘ 𝐴 ) − 1 ) ) = ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) )
101 31 99 100 syl2anc ⊢ ( 𝜑 → ( 𝐴 prefix ( ( ♯ ‘ 𝐴 ) − 1 ) ) = ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) )
102 101 fveq2d ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐴 prefix ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) = ( ♯ ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) )
103 pfxlen ⊢ ( ( 𝐴 ∈ Word 𝑊 ∧ ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) → ( ♯ ‘ ( 𝐴 prefix ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) = ( ( ♯ ‘ 𝐴 ) − 1 ) )
104 31 99 103 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐴 prefix ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) = ( ( ♯ ‘ 𝐴 ) − 1 ) )
105 102 104 eqtr3d ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) = ( ( ♯ ‘ 𝐴 ) − 1 ) )
106 105 oveq1d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) − 1 ) = ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) )
107 106 12 eqtr4di ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) − 1 ) = 𝐾 )
108 107 fveq2d ⊢ ( 𝜑 → ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ ( ( ♯ ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) − 1 ) ) = ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ 𝐾 ) )
109 45 fvresd ⊢ ( 𝜑 → ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ 𝐾 ) = ( 𝐴 ‘ 𝐾 ) )
110 97 108 109 3eqtrd ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) = ( 𝐴 ‘ 𝐾 ) )
111 110 fveq2d ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) ) = ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) )
112 1 2 3 4 5 6 efgsdmi ⊢ ( ( 𝐴 ∈ dom 𝑆 ∧ ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ℕ ) → ( 𝑆 ‘ 𝐴 ) ∈ ran ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) )
113 8 42 112 syl2anc ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐴 ) ∈ ran ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) )
114 12 fveq2i ⊢ ( 𝐴 ‘ 𝐾 ) = ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) )
115 114 fveq2i ⊢ ( 𝑇 ‘ ( 𝐴 ‘ 𝐾 ) ) = ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) )
116 115 rneqi ⊢ ran ( 𝑇 ‘ ( 𝐴 ‘ 𝐾 ) ) = ran ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) )
117 113 116 eleqtrrdi ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐴 ) ∈ ran ( 𝑇 ‘ ( 𝐴 ‘ 𝐾 ) ) )
118 1 2 3 4 efgtlen ⊢ ( ( ( 𝐴 ‘ 𝐾 ) ∈ 𝑊 ∧ ( 𝑆 ‘ 𝐴 ) ∈ ran ( 𝑇 ‘ ( 𝐴 ‘ 𝐾 ) ) ) → ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) = ( ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) + 2 ) )
119 47 117 118 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) = ( ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) + 2 ) )
120 88 111 119 3brtr4d ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) )
121 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 efgredleme ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝐾 ) ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐶 ) ) ∧ ( 𝐵 ‘ 𝐿 ) ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐶 ) ) ) )
122 121 simpld ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐾 ) ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐶 ) ) )
123 1 2 3 4 5 6 efgsp1 ⊢ ( ( 𝐶 ∈ dom 𝑆 ∧ ( 𝐴 ‘ 𝐾 ) ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐶 ) ) ) → ( 𝐶 ++ ⟨“ ( 𝐴 ‘ 𝐾 ) ”⟩ ) ∈ dom 𝑆 )
124 22 122 123 syl2anc ⊢ ( 𝜑 → ( 𝐶 ++ ⟨“ ( 𝐴 ‘ 𝐾 ) ”⟩ ) ∈ dom 𝑆 )
125 1 2 3 4 5 6 efgsval2 ⊢ ( ( 𝐶 ∈ Word 𝑊 ∧ ( 𝐴 ‘ 𝐾 ) ∈ 𝑊 ∧ ( 𝐶 ++ ⟨“ ( 𝐴 ‘ 𝐾 ) ”⟩ ) ∈ dom 𝑆 ) → ( 𝑆 ‘ ( 𝐶 ++ ⟨“ ( 𝐴 ‘ 𝐾 ) ”⟩ ) ) = ( 𝐴 ‘ 𝐾 ) )
126 27 47 124 125 syl3anc ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐶 ++ ⟨“ ( 𝐴 ‘ 𝐾 ) ”⟩ ) ) = ( 𝐴 ‘ 𝐾 ) )
127 110 126 eqtr4d ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) = ( 𝑆 ‘ ( 𝐶 ++ ⟨“ ( 𝐴 ‘ 𝐾 ) ”⟩ ) ) )
128 2fveq3 ⊢ ( 𝑎 = ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) → ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) = ( ♯ ‘ ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) ) )
129 128 breq1d ⊢ ( 𝑎 = ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) → ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) ↔ ( ♯ ‘ ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) ) )
130 fveqeq2 ⊢ ( 𝑎 = ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) ↔ ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) = ( 𝑆 ‘ 𝑏 ) ) )
131 fveq1 ⊢ ( 𝑎 = ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) → ( 𝑎 ‘ 0 ) = ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ 0 ) )
132 131 eqeq1d ⊢ ( 𝑎 = ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) → ( ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ↔ ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ 0 ) = ( 𝑏 ‘ 0 ) ) )
133 130 132 imbi12d ⊢ ( 𝑎 = ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) → ( ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ↔ ( ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) = ( 𝑆 ‘ 𝑏 ) → ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) )
134 129 133 imbi12d ⊢ ( 𝑎 = ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) → ( ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ↔ ( ( ♯ ‘ ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) → ( ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) = ( 𝑆 ‘ 𝑏 ) → ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ) )
135 fveq2 ⊢ ( 𝑏 = ( 𝐶 ++ ⟨“ ( 𝐴 ‘ 𝐾 ) ”⟩ ) → ( 𝑆 ‘ 𝑏 ) = ( 𝑆 ‘ ( 𝐶 ++ ⟨“ ( 𝐴 ‘ 𝐾 ) ”⟩ ) ) )
136 135 eqeq2d ⊢ ( 𝑏 = ( 𝐶 ++ ⟨“ ( 𝐴 ‘ 𝐾 ) ”⟩ ) → ( ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) = ( 𝑆 ‘ 𝑏 ) ↔ ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) = ( 𝑆 ‘ ( 𝐶 ++ ⟨“ ( 𝐴 ‘ 𝐾 ) ”⟩ ) ) ) )
137 fveq1 ⊢ ( 𝑏 = ( 𝐶 ++ ⟨“ ( 𝐴 ‘ 𝐾 ) ”⟩ ) → ( 𝑏 ‘ 0 ) = ( ( 𝐶 ++ ⟨“ ( 𝐴 ‘ 𝐾 ) ”⟩ ) ‘ 0 ) )
138 137 eqeq2d ⊢ ( 𝑏 = ( 𝐶 ++ ⟨“ ( 𝐴 ‘ 𝐾 ) ”⟩ ) → ( ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ 0 ) = ( 𝑏 ‘ 0 ) ↔ ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ 0 ) = ( ( 𝐶 ++ ⟨“ ( 𝐴 ‘ 𝐾 ) ”⟩ ) ‘ 0 ) ) )
139 136 138 imbi12d ⊢ ( 𝑏 = ( 𝐶 ++ ⟨“ ( 𝐴 ‘ 𝐾 ) ”⟩ ) → ( ( ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) = ( 𝑆 ‘ 𝑏 ) → ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ↔ ( ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) = ( 𝑆 ‘ ( 𝐶 ++ ⟨“ ( 𝐴 ‘ 𝐾 ) ”⟩ ) ) → ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ 0 ) = ( ( 𝐶 ++ ⟨“ ( 𝐴 ‘ 𝐾 ) ”⟩ ) ‘ 0 ) ) ) )
140 139 imbi2d ⊢ ( 𝑏 = ( 𝐶 ++ ⟨“ ( 𝐴 ‘ 𝐾 ) ”⟩ ) → ( ( ( ♯ ‘ ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) → ( ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) = ( 𝑆 ‘ 𝑏 ) → ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ↔ ( ( ♯ ‘ ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) → ( ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) = ( 𝑆 ‘ ( 𝐶 ++ ⟨“ ( 𝐴 ‘ 𝐾 ) ”⟩ ) ) → ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ 0 ) = ( ( 𝐶 ++ ⟨“ ( 𝐴 ‘ 𝐾 ) ”⟩ ) ‘ 0 ) ) ) ) )
141 134 140 rspc2va ⊢ ( ( ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ∈ dom 𝑆 ∧ ( 𝐶 ++ ⟨“ ( 𝐴 ‘ 𝐾 ) ”⟩ ) ∈ dom 𝑆 ) ∧ ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ) → ( ( ♯ ‘ ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) → ( ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) = ( 𝑆 ‘ ( 𝐶 ++ ⟨“ ( 𝐴 ‘ 𝐾 ) ”⟩ ) ) → ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ 0 ) = ( ( 𝐶 ++ ⟨“ ( 𝐴 ‘ 𝐾 ) ”⟩ ) ‘ 0 ) ) ) )
142 95 124 7 141 syl21anc ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) → ( ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) = ( 𝑆 ‘ ( 𝐶 ++ ⟨“ ( 𝐴 ‘ 𝐾 ) ”⟩ ) ) → ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ 0 ) = ( ( 𝐶 ++ ⟨“ ( 𝐴 ‘ 𝐾 ) ”⟩ ) ‘ 0 ) ) ) )
143 120 127 142 mp2d ⊢ ( 𝜑 → ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ 0 ) = ( ( 𝐶 ++ ⟨“ ( 𝐴 ‘ 𝐾 ) ”⟩ ) ‘ 0 ) )
144 81 75 sseldi ⊢ ( 𝜑 → ( 𝐵 ‘ 𝐿 ) ∈ Word ( 𝐼 × 2o ) )
145 lencl ⊢ ( ( 𝐵 ‘ 𝐿 ) ∈ Word ( 𝐼 × 2o ) → ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ∈ ℕ0 )
146 144 145 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ∈ ℕ0 )
147 146 nn0red ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ∈ ℝ )
148 ltaddrp ⊢ ( ( ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ∈ ℝ ∧ 2 ∈ ℝ+ ) → ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) < ( ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) + 2 ) )
149 147 86 148 sylancl ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) < ( ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) + 2 ) )
150 65 nn0red ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℝ )
151 150 lem1d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐵 ) − 1 ) ≤ ( ♯ ‘ 𝐵 ) )
152 fznn ⊢ ( ( ♯ ‘ 𝐵 ) ∈ ℤ → ( ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ↔ ( ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ℕ ∧ ( ( ♯ ‘ 𝐵 ) − 1 ) ≤ ( ♯ ‘ 𝐵 ) ) ) )
153 66 152 syl ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ↔ ( ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ℕ ∧ ( ( ♯ ‘ 𝐵 ) − 1 ) ≤ ( ♯ ‘ 𝐵 ) ) ) )
154 70 151 153 mpbir2and ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) )
155 1 2 3 4 5 6 efgsres ⊢ ( ( 𝐵 ∈ dom 𝑆 ∧ ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ) → ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ∈ dom 𝑆 )
156 9 154 155 syl2anc ⊢ ( 𝜑 → ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ∈ dom 𝑆 )
157 1 2 3 4 5 6 efgsval ⊢ ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ∈ dom 𝑆 → ( 𝑆 ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) = ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ‘ ( ( ♯ ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) − 1 ) ) )
158 156 157 syl ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) = ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ‘ ( ( ♯ ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) − 1 ) ) )
159 fz1ssfz0 ⊢ ( 1 ... ( ♯ ‘ 𝐵 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝐵 ) )
160 159 154 sseldi ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐵 ) ) )
161 pfxres ⊢ ( ( 𝐵 ∈ Word 𝑊 ∧ ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐵 ) ) ) → ( 𝐵 prefix ( ( ♯ ‘ 𝐵 ) − 1 ) ) = ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) )
162 60 160 161 syl2anc ⊢ ( 𝜑 → ( 𝐵 prefix ( ( ♯ ‘ 𝐵 ) − 1 ) ) = ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) )
163 162 fveq2d ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐵 prefix ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) = ( ♯ ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) )
164 pfxlen ⊢ ( ( 𝐵 ∈ Word 𝑊 ∧ ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐵 ) ) ) → ( ♯ ‘ ( 𝐵 prefix ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) = ( ( ♯ ‘ 𝐵 ) − 1 ) )
165 60 160 164 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐵 prefix ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) = ( ( ♯ ‘ 𝐵 ) − 1 ) )
166 163 165 eqtr3d ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) = ( ( ♯ ‘ 𝐵 ) − 1 ) )
167 166 oveq1d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) − 1 ) = ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) )
168 167 13 eqtr4di ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) − 1 ) = 𝐿 )
169 168 fveq2d ⊢ ( 𝜑 → ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ‘ ( ( ♯ ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) − 1 ) ) = ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ‘ 𝐿 ) )
170 73 fvresd ⊢ ( 𝜑 → ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ‘ 𝐿 ) = ( 𝐵 ‘ 𝐿 ) )
171 158 169 170 3eqtrd ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) = ( 𝐵 ‘ 𝐿 ) )
172 171 fveq2d ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑆 ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) ) = ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) )
173 1 2 3 4 5 6 efgsdmi ⊢ ( ( 𝐵 ∈ dom 𝑆 ∧ ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ℕ ) → ( 𝑆 ‘ 𝐵 ) ∈ ran ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) )
174 9 70 173 syl2anc ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐵 ) ∈ ran ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) )
175 10 174 eqeltrd ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐴 ) ∈ ran ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) )
176 13 fveq2i ⊢ ( 𝐵 ‘ 𝐿 ) = ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) )
177 176 fveq2i ⊢ ( 𝑇 ‘ ( 𝐵 ‘ 𝐿 ) ) = ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) )
178 177 rneqi ⊢ ran ( 𝑇 ‘ ( 𝐵 ‘ 𝐿 ) ) = ran ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) )
179 175 178 eleqtrrdi ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐴 ) ∈ ran ( 𝑇 ‘ ( 𝐵 ‘ 𝐿 ) ) )
180 1 2 3 4 efgtlen ⊢ ( ( ( 𝐵 ‘ 𝐿 ) ∈ 𝑊 ∧ ( 𝑆 ‘ 𝐴 ) ∈ ran ( 𝑇 ‘ ( 𝐵 ‘ 𝐿 ) ) ) → ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) = ( ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) + 2 ) )
181 75 179 180 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) = ( ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) + 2 ) )
182 149 172 181 3brtr4d ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑆 ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) )
183 121 simprd ⊢ ( 𝜑 → ( 𝐵 ‘ 𝐿 ) ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐶 ) ) )
184 1 2 3 4 5 6 efgsp1 ⊢ ( ( 𝐶 ∈ dom 𝑆 ∧ ( 𝐵 ‘ 𝐿 ) ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐶 ) ) ) → ( 𝐶 ++ ⟨“ ( 𝐵 ‘ 𝐿 ) ”⟩ ) ∈ dom 𝑆 )
185 22 183 184 syl2anc ⊢ ( 𝜑 → ( 𝐶 ++ ⟨“ ( 𝐵 ‘ 𝐿 ) ”⟩ ) ∈ dom 𝑆 )
186 1 2 3 4 5 6 efgsval2 ⊢ ( ( 𝐶 ∈ Word 𝑊 ∧ ( 𝐵 ‘ 𝐿 ) ∈ 𝑊 ∧ ( 𝐶 ++ ⟨“ ( 𝐵 ‘ 𝐿 ) ”⟩ ) ∈ dom 𝑆 ) → ( 𝑆 ‘ ( 𝐶 ++ ⟨“ ( 𝐵 ‘ 𝐿 ) ”⟩ ) ) = ( 𝐵 ‘ 𝐿 ) )
187 27 75 185 186 syl3anc ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐶 ++ ⟨“ ( 𝐵 ‘ 𝐿 ) ”⟩ ) ) = ( 𝐵 ‘ 𝐿 ) )
188 171 187 eqtr4d ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) = ( 𝑆 ‘ ( 𝐶 ++ ⟨“ ( 𝐵 ‘ 𝐿 ) ”⟩ ) ) )
189 2fveq3 ⊢ ( 𝑎 = ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) = ( ♯ ‘ ( 𝑆 ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) ) )
190 189 breq1d ⊢ ( 𝑎 = ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) ↔ ( ♯ ‘ ( 𝑆 ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) ) )
191 fveqeq2 ⊢ ( 𝑎 = ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) ↔ ( 𝑆 ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) = ( 𝑆 ‘ 𝑏 ) ) )
192 fveq1 ⊢ ( 𝑎 = ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → ( 𝑎 ‘ 0 ) = ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ‘ 0 ) )
193 192 eqeq1d ⊢ ( 𝑎 = ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → ( ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ↔ ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ‘ 0 ) = ( 𝑏 ‘ 0 ) ) )
194 191 193 imbi12d ⊢ ( 𝑎 = ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → ( ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ↔ ( ( 𝑆 ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) = ( 𝑆 ‘ 𝑏 ) → ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) )
195 190 194 imbi12d ⊢ ( 𝑎 = ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → ( ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ↔ ( ( ♯ ‘ ( 𝑆 ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) → ( ( 𝑆 ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) = ( 𝑆 ‘ 𝑏 ) → ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ) )
196 fveq2 ⊢ ( 𝑏 = ( 𝐶 ++ ⟨“ ( 𝐵 ‘ 𝐿 ) ”⟩ ) → ( 𝑆 ‘ 𝑏 ) = ( 𝑆 ‘ ( 𝐶 ++ ⟨“ ( 𝐵 ‘ 𝐿 ) ”⟩ ) ) )
197 196 eqeq2d ⊢ ( 𝑏 = ( 𝐶 ++ ⟨“ ( 𝐵 ‘ 𝐿 ) ”⟩ ) → ( ( 𝑆 ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) = ( 𝑆 ‘ 𝑏 ) ↔ ( 𝑆 ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) = ( 𝑆 ‘ ( 𝐶 ++ ⟨“ ( 𝐵 ‘ 𝐿 ) ”⟩ ) ) ) )
198 fveq1 ⊢ ( 𝑏 = ( 𝐶 ++ ⟨“ ( 𝐵 ‘ 𝐿 ) ”⟩ ) → ( 𝑏 ‘ 0 ) = ( ( 𝐶 ++ ⟨“ ( 𝐵 ‘ 𝐿 ) ”⟩ ) ‘ 0 ) )
199 198 eqeq2d ⊢ ( 𝑏 = ( 𝐶 ++ ⟨“ ( 𝐵 ‘ 𝐿 ) ”⟩ ) → ( ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ‘ 0 ) = ( 𝑏 ‘ 0 ) ↔ ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ‘ 0 ) = ( ( 𝐶 ++ ⟨“ ( 𝐵 ‘ 𝐿 ) ”⟩ ) ‘ 0 ) ) )
200 197 199 imbi12d ⊢ ( 𝑏 = ( 𝐶 ++ ⟨“ ( 𝐵 ‘ 𝐿 ) ”⟩ ) → ( ( ( 𝑆 ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) = ( 𝑆 ‘ 𝑏 ) → ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ↔ ( ( 𝑆 ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) = ( 𝑆 ‘ ( 𝐶 ++ ⟨“ ( 𝐵 ‘ 𝐿 ) ”⟩ ) ) → ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ‘ 0 ) = ( ( 𝐶 ++ ⟨“ ( 𝐵 ‘ 𝐿 ) ”⟩ ) ‘ 0 ) ) ) )
201 200 imbi2d ⊢ ( 𝑏 = ( 𝐶 ++ ⟨“ ( 𝐵 ‘ 𝐿 ) ”⟩ ) → ( ( ( ♯ ‘ ( 𝑆 ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) → ( ( 𝑆 ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) = ( 𝑆 ‘ 𝑏 ) → ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ↔ ( ( ♯ ‘ ( 𝑆 ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) → ( ( 𝑆 ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) = ( 𝑆 ‘ ( 𝐶 ++ ⟨“ ( 𝐵 ‘ 𝐿 ) ”⟩ ) ) → ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ‘ 0 ) = ( ( 𝐶 ++ ⟨“ ( 𝐵 ‘ 𝐿 ) ”⟩ ) ‘ 0 ) ) ) ) )
202 195 201 rspc2va ⊢ ( ( ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ∈ dom 𝑆 ∧ ( 𝐶 ++ ⟨“ ( 𝐵 ‘ 𝐿 ) ”⟩ ) ∈ dom 𝑆 ) ∧ ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ) → ( ( ♯ ‘ ( 𝑆 ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) → ( ( 𝑆 ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) = ( 𝑆 ‘ ( 𝐶 ++ ⟨“ ( 𝐵 ‘ 𝐿 ) ”⟩ ) ) → ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ‘ 0 ) = ( ( 𝐶 ++ ⟨“ ( 𝐵 ‘ 𝐿 ) ”⟩ ) ‘ 0 ) ) ) )
203 156 185 7 202 syl21anc ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝑆 ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) → ( ( 𝑆 ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) = ( 𝑆 ‘ ( 𝐶 ++ ⟨“ ( 𝐵 ‘ 𝐿 ) ”⟩ ) ) → ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ‘ 0 ) = ( ( 𝐶 ++ ⟨“ ( 𝐵 ‘ 𝐿 ) ”⟩ ) ‘ 0 ) ) ) )
204 182 188 203 mp2d ⊢ ( 𝜑 → ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ‘ 0 ) = ( ( 𝐶 ++ ⟨“ ( 𝐵 ‘ 𝐿 ) ”⟩ ) ‘ 0 ) )
205 79 143 204 3eqtr4d ⊢ ( 𝜑 → ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ 0 ) = ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ‘ 0 ) )
206 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ↔ ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ℕ )
207 42 206 sylibr ⊢ ( 𝜑 → 0 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) )
208 207 fvresd ⊢ ( 𝜑 → ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ 0 ) = ( 𝐴 ‘ 0 ) )
209 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ↔ ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ℕ )
210 70 209 sylibr ⊢ ( 𝜑 → 0 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) )
211 210 fvresd ⊢ ( 𝜑 → ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ‘ 0 ) = ( 𝐵 ‘ 0 ) )
212 205 208 211 3eqtr3d ⊢ ( 𝜑 → ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) )