Metamath Proof Explorer

Theorem efgredlem

Description: The reduced word that forms the base of the sequence in efgsval is uniquely determined, given the ending representation. (Contributed by Mario Carneiro, 30-Sep-2015) (Proof shortened by AV, 3-Nov-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 ) )
Assertion efgredlem ¬ 𝜑

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 fviss ⊢ ( I ‘ Word ( 𝐼 × 2o ) ) ⊆ Word ( 𝐼 × 2o )
13 1 12 eqsstri ⊢ 𝑊 ⊆ Word ( 𝐼 × 2o )
14 1 2 3 4 5 6 efgsdm ⊢ ( 𝐴 ∈ dom 𝑆 ↔ ( 𝐴 ∈ ( Word 𝑊 ∖ { ∅ } ) ∧ ( 𝐴 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝐴 ) ) ( 𝐴 ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( 𝐴 ‘ ( 𝑖 − 1 ) ) ) ) )
15 14 simp1bi ⊢ ( 𝐴 ∈ dom 𝑆 → 𝐴 ∈ ( Word 𝑊 ∖ { ∅ } ) )
16 8 15 syl ⊢ ( 𝜑 → 𝐴 ∈ ( Word 𝑊 ∖ { ∅ } ) )
17 16 eldifad ⊢ ( 𝜑 → 𝐴 ∈ Word 𝑊 )
18 wrdf ⊢ ( 𝐴 ∈ Word 𝑊 → 𝐴 : ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ⟶ 𝑊 )
19 17 18 syl ⊢ ( 𝜑 → 𝐴 : ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ⟶ 𝑊 )
20 1 2 3 4 5 6 7 8 9 10 11 efgredlema ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ℕ ∧ ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ℕ ) )
21 20 simpld ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ℕ )
22 nnm1nn0 ⊢ ( ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ℕ → ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ∈ ℕ0 )
23 21 22 syl ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ∈ ℕ0 )
24 21 nnred ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ℝ )
25 24 lem1d ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ≤ ( ( ♯ ‘ 𝐴 ) − 1 ) )
26 eldifsni ⊢ ( 𝐴 ∈ ( Word 𝑊 ∖ { ∅ } ) → 𝐴 ≠ ∅ )
27 8 15 26 3syl ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
28 wrdfin ⊢ ( 𝐴 ∈ Word 𝑊 → 𝐴 ∈ Fin )
29 hashnncl ⊢ ( 𝐴 ∈ Fin → ( ( ♯ ‘ 𝐴 ) ∈ ℕ ↔ 𝐴 ≠ ∅ ) )
30 17 28 29 3syl ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) ∈ ℕ ↔ 𝐴 ≠ ∅ ) )
31 27 30 mpbird ⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ℕ )
32 nnm1nn0 ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ → ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ℕ0 )
33 fznn0 ⊢ ( ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ℕ0 → ( ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ∈ ( 0 ... ( ( ♯ ‘ 𝐴 ) − 1 ) ) ↔ ( ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ∈ ℕ0 ∧ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ≤ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) )
34 31 32 33 3syl ⊢ ( 𝜑 → ( ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ∈ ( 0 ... ( ( ♯ ‘ 𝐴 ) − 1 ) ) ↔ ( ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ∈ ℕ0 ∧ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ≤ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) )
35 23 25 34 mpbir2and ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ∈ ( 0 ... ( ( ♯ ‘ 𝐴 ) − 1 ) ) )
36 lencl ⊢ ( 𝐴 ∈ Word 𝑊 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
37 17 36 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
38 37 nn0zd ⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ℤ )
39 fzoval ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℤ → ( 0 ..^ ( ♯ ‘ 𝐴 ) ) = ( 0 ... ( ( ♯ ‘ 𝐴 ) − 1 ) ) )
40 38 39 syl ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐴 ) ) = ( 0 ... ( ( ♯ ‘ 𝐴 ) − 1 ) ) )
41 35 40 eleqtrrd ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) )
42 19 41 ffvelrnd ⊢ ( 𝜑 → ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ∈ 𝑊 )
43 13 42 sselid ⊢ ( 𝜑 → ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ∈ Word ( 𝐼 × 2o ) )
44 lencl ⊢ ( ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ∈ Word ( 𝐼 × 2o ) → ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ∈ ℕ0 )
45 43 44 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ∈ ℕ0 )
46 45 nn0red ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ∈ ℝ )
47 2rp ⊢ 2 ∈ ℝ+
48 ltaddrp ⊢ ( ( ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ∈ ℝ ∧ 2 ∈ ℝ+ ) → ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) < ( ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) + 2 ) )
49 46 47 48 sylancl ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) < ( ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) + 2 ) )
50 37 nn0red ⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ℝ )
51 50 lem1d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) − 1 ) ≤ ( ♯ ‘ 𝐴 ) )
52 fznn ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℤ → ( ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ↔ ( ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ℕ ∧ ( ( ♯ ‘ 𝐴 ) − 1 ) ≤ ( ♯ ‘ 𝐴 ) ) ) )
53 38 52 syl ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ↔ ( ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ℕ ∧ ( ( ♯ ‘ 𝐴 ) − 1 ) ≤ ( ♯ ‘ 𝐴 ) ) ) )
54 21 51 53 mpbir2and ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) )
55 1 2 3 4 5 6 efgsres ⊢ ( ( 𝐴 ∈ dom 𝑆 ∧ ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ∈ dom 𝑆 )
56 8 54 55 syl2anc ⊢ ( 𝜑 → ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ∈ dom 𝑆 )
57 1 2 3 4 5 6 efgsval ⊢ ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ∈ dom 𝑆 → ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) = ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ ( ( ♯ ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) − 1 ) ) )
58 56 57 syl ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) = ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ ( ( ♯ ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) − 1 ) ) )
59 fz1ssfz0 ⊢ ( 1 ... ( ♯ ‘ 𝐴 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝐴 ) )
60 59 54 sselid ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) )
61 pfxres ⊢ ( ( 𝐴 ∈ Word 𝑊 ∧ ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐴 prefix ( ( ♯ ‘ 𝐴 ) − 1 ) ) = ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) )
62 17 60 61 syl2anc ⊢ ( 𝜑 → ( 𝐴 prefix ( ( ♯ ‘ 𝐴 ) − 1 ) ) = ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) )
63 62 fveq2d ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐴 prefix ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) = ( ♯ ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) )
64 pfxlen ⊢ ( ( 𝐴 ∈ Word 𝑊 ∧ ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) → ( ♯ ‘ ( 𝐴 prefix ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) = ( ( ♯ ‘ 𝐴 ) − 1 ) )
65 17 60 64 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐴 prefix ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) = ( ( ♯ ‘ 𝐴 ) − 1 ) )
66 63 65 eqtr3d ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) = ( ( ♯ ‘ 𝐴 ) − 1 ) )
67 66 fvoveq1d ⊢ ( 𝜑 → ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ ( ( ♯ ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) − 1 ) ) = ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) )
68 fzo0end ⊢ ( ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ℕ → ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) )
69 fvres ⊢ ( ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) → ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) = ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) )
70 21 68 69 3syl ⊢ ( 𝜑 → ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) = ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) )
71 58 67 70 3eqtrd ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) = ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) )
72 71 fveq2d ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) ) = ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) )
73 1 2 3 4 5 6 efgsdmi ⊢ ( ( 𝐴 ∈ dom 𝑆 ∧ ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ℕ ) → ( 𝑆 ‘ 𝐴 ) ∈ ran ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) )
74 8 21 73 syl2anc ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐴 ) ∈ ran ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) )
75 1 2 3 4 efgtlen ⊢ ( ( ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ∈ 𝑊 ∧ ( 𝑆 ‘ 𝐴 ) ∈ ran ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) → ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) = ( ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) + 2 ) )
76 42 74 75 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) = ( ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) + 2 ) )
77 49 72 76 3brtr4d ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) )
78 1 2 3 4 efgtf ⊢ ( ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ∈ 𝑊 → ( ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) ∧ ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) : ( ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 ) )
79 42 78 syl ⊢ ( 𝜑 → ( ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) ∧ ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) : ( ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 ) )
80 79 simprd ⊢ ( 𝜑 → ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) : ( ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 )
81 ffn ⊢ ( ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) : ( ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 → ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) Fn ( ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) × ( 𝐼 × 2o ) ) )
82 ovelrn ⊢ ( ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) Fn ( ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) × ( 𝐼 × 2o ) ) → ( ( 𝑆 ‘ 𝐴 ) ∈ ran ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ↔ ∃ 𝑖 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) ∃ 𝑟 ∈ ( 𝐼 × 2o ) ( 𝑆 ‘ 𝐴 ) = ( 𝑖 ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) 𝑟 ) ) )
83 80 81 82 3syl ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐴 ) ∈ ran ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ↔ ∃ 𝑖 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) ∃ 𝑟 ∈ ( 𝐼 × 2o ) ( 𝑆 ‘ 𝐴 ) = ( 𝑖 ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) 𝑟 ) ) )
84 74 83 mpbid ⊢ ( 𝜑 → ∃ 𝑖 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) ∃ 𝑟 ∈ ( 𝐼 × 2o ) ( 𝑆 ‘ 𝐴 ) = ( 𝑖 ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) 𝑟 ) )
85 20 simprd ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ℕ )
86 1 2 3 4 5 6 efgsdmi ⊢ ( ( 𝐵 ∈ dom 𝑆 ∧ ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ℕ ) → ( 𝑆 ‘ 𝐵 ) ∈ ran ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) )
87 9 85 86 syl2anc ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐵 ) ∈ ran ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) )
88 1 2 3 4 5 6 efgsdm ⊢ ( 𝐵 ∈ dom 𝑆 ↔ ( 𝐵 ∈ ( Word 𝑊 ∖ { ∅ } ) ∧ ( 𝐵 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝐵 ) ) ( 𝐵 ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( 𝐵 ‘ ( 𝑖 − 1 ) ) ) ) )
89 88 simp1bi ⊢ ( 𝐵 ∈ dom 𝑆 → 𝐵 ∈ ( Word 𝑊 ∖ { ∅ } ) )
90 9 89 syl ⊢ ( 𝜑 → 𝐵 ∈ ( Word 𝑊 ∖ { ∅ } ) )
91 90 eldifad ⊢ ( 𝜑 → 𝐵 ∈ Word 𝑊 )
92 wrdf ⊢ ( 𝐵 ∈ Word 𝑊 → 𝐵 : ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ⟶ 𝑊 )
93 91 92 syl ⊢ ( 𝜑 → 𝐵 : ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ⟶ 𝑊 )
94 fzo0end ⊢ ( ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ℕ → ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) )
95 elfzofz ⊢ ( ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) → ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ∈ ( 0 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) )
96 85 94 95 3syl ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ∈ ( 0 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) )
97 lencl ⊢ ( 𝐵 ∈ Word 𝑊 → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
98 91 97 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
99 98 nn0zd ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℤ )
100 fzoval ⊢ ( ( ♯ ‘ 𝐵 ) ∈ ℤ → ( 0 ..^ ( ♯ ‘ 𝐵 ) ) = ( 0 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) )
101 99 100 syl ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐵 ) ) = ( 0 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) )
102 96 101 eleqtrrd ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) )
103 93 102 ffvelrnd ⊢ ( 𝜑 → ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ∈ 𝑊 )
104 1 2 3 4 efgtf ⊢ ( ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ∈ 𝑊 → ( ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) ∧ ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) : ( ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 ) )
105 103 104 syl ⊢ ( 𝜑 → ( ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) ∧ ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) : ( ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 ) )
106 105 simprd ⊢ ( 𝜑 → ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) : ( ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 )
107 ffn ⊢ ( ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) : ( ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 → ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) Fn ( ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) × ( 𝐼 × 2o ) ) )
108 ovelrn ⊢ ( ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) Fn ( ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) × ( 𝐼 × 2o ) ) → ( ( 𝑆 ‘ 𝐵 ) ∈ ran ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ↔ ∃ 𝑗 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) ∃ 𝑠 ∈ ( 𝐼 × 2o ) ( 𝑆 ‘ 𝐵 ) = ( 𝑗 ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) 𝑠 ) ) )
109 106 107 108 3syl ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐵 ) ∈ ran ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ↔ ∃ 𝑗 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) ∃ 𝑠 ∈ ( 𝐼 × 2o ) ( 𝑆 ‘ 𝐵 ) = ( 𝑗 ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) 𝑠 ) ) )
110 87 109 mpbid ⊢ ( 𝜑 → ∃ 𝑗 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) ∃ 𝑠 ∈ ( 𝐼 × 2o ) ( 𝑆 ‘ 𝐵 ) = ( 𝑗 ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) 𝑠 ) )
111 reeanv ⊢ ( ∃ 𝑖 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) ∃ 𝑗 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) ( ∃ 𝑟 ∈ ( 𝐼 × 2o ) ( 𝑆 ‘ 𝐴 ) = ( 𝑖 ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) 𝑟 ) ∧ ∃ 𝑠 ∈ ( 𝐼 × 2o ) ( 𝑆 ‘ 𝐵 ) = ( 𝑗 ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) 𝑠 ) ) ↔ ( ∃ 𝑖 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) ∃ 𝑟 ∈ ( 𝐼 × 2o ) ( 𝑆 ‘ 𝐴 ) = ( 𝑖 ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) 𝑟 ) ∧ ∃ 𝑗 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) ∃ 𝑠 ∈ ( 𝐼 × 2o ) ( 𝑆 ‘ 𝐵 ) = ( 𝑗 ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) 𝑠 ) ) )
112 reeanv ⊢ ( ∃ 𝑟 ∈ ( 𝐼 × 2o ) ∃ 𝑠 ∈ ( 𝐼 × 2o ) ( ( 𝑆 ‘ 𝐴 ) = ( 𝑖 ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) 𝑟 ) ∧ ( 𝑆 ‘ 𝐵 ) = ( 𝑗 ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) 𝑠 ) ) ↔ ( ∃ 𝑟 ∈ ( 𝐼 × 2o ) ( 𝑆 ‘ 𝐴 ) = ( 𝑖 ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) 𝑟 ) ∧ ∃ 𝑠 ∈ ( 𝐼 × 2o ) ( 𝑆 ‘ 𝐵 ) = ( 𝑗 ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) 𝑠 ) ) )
113 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) ) ) ∧ ( ( 𝑟 ∈ ( 𝐼 × 2o ) ∧ 𝑠 ∈ ( 𝐼 × 2o ) ) ∧ ( ( 𝑆 ‘ 𝐴 ) = ( 𝑖 ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) 𝑟 ) ∧ ( 𝑆 ‘ 𝐵 ) = ( 𝑗 ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) 𝑠 ) ) ) ) ∧ ¬ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) = ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) → ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) )
114 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) ) ) ∧ ( ( 𝑟 ∈ ( 𝐼 × 2o ) ∧ 𝑠 ∈ ( 𝐼 × 2o ) ) ∧ ( ( 𝑆 ‘ 𝐴 ) = ( 𝑖 ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) 𝑟 ) ∧ ( 𝑆 ‘ 𝐵 ) = ( 𝑗 ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) 𝑠 ) ) ) ) ∧ ¬ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) = ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) → 𝐴 ∈ dom 𝑆 )
115 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) ) ) ∧ ( ( 𝑟 ∈ ( 𝐼 × 2o ) ∧ 𝑠 ∈ ( 𝐼 × 2o ) ) ∧ ( ( 𝑆 ‘ 𝐴 ) = ( 𝑖 ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) 𝑟 ) ∧ ( 𝑆 ‘ 𝐵 ) = ( 𝑗 ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) 𝑠 ) ) ) ) ∧ ¬ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) = ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) → 𝐵 ∈ dom 𝑆 )
116 10 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) ) ) ∧ ( ( 𝑟 ∈ ( 𝐼 × 2o ) ∧ 𝑠 ∈ ( 𝐼 × 2o ) ) ∧ ( ( 𝑆 ‘ 𝐴 ) = ( 𝑖 ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) 𝑟 ) ∧ ( 𝑆 ‘ 𝐵 ) = ( 𝑗 ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) 𝑠 ) ) ) ) ∧ ¬ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) = ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) → ( 𝑆 ‘ 𝐴 ) = ( 𝑆 ‘ 𝐵 ) )
117 11 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) ) ) ∧ ( ( 𝑟 ∈ ( 𝐼 × 2o ) ∧ 𝑠 ∈ ( 𝐼 × 2o ) ) ∧ ( ( 𝑆 ‘ 𝐴 ) = ( 𝑖 ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) 𝑟 ) ∧ ( 𝑆 ‘ 𝐵 ) = ( 𝑗 ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) 𝑠 ) ) ) ) ∧ ¬ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) = ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) → ¬ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) )
118 eqid ⊢ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) = ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 )
119 eqid ⊢ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) = ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 )
120 simpllr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) ) ) ∧ ( ( 𝑟 ∈ ( 𝐼 × 2o ) ∧ 𝑠 ∈ ( 𝐼 × 2o ) ) ∧ ( ( 𝑆 ‘ 𝐴 ) = ( 𝑖 ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) 𝑟 ) ∧ ( 𝑆 ‘ 𝐵 ) = ( 𝑗 ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) 𝑠 ) ) ) ) ∧ ¬ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) = ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) → ( 𝑖 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) ) )
121 120 simpld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) ) ) ∧ ( ( 𝑟 ∈ ( 𝐼 × 2o ) ∧ 𝑠 ∈ ( 𝐼 × 2o ) ) ∧ ( ( 𝑆 ‘ 𝐴 ) = ( 𝑖 ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) 𝑟 ) ∧ ( 𝑆 ‘ 𝐵 ) = ( 𝑗 ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) 𝑠 ) ) ) ) ∧ ¬ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) = ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) → 𝑖 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) )
122 120 simprd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) ) ) ∧ ( ( 𝑟 ∈ ( 𝐼 × 2o ) ∧ 𝑠 ∈ ( 𝐼 × 2o ) ) ∧ ( ( 𝑆 ‘ 𝐴 ) = ( 𝑖 ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) 𝑟 ) ∧ ( 𝑆 ‘ 𝐵 ) = ( 𝑗 ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) 𝑠 ) ) ) ) ∧ ¬ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) = ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) → 𝑗 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) )
123 simplrl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) ) ) ∧ ( ( 𝑟 ∈ ( 𝐼 × 2o ) ∧ 𝑠 ∈ ( 𝐼 × 2o ) ) ∧ ( ( 𝑆 ‘ 𝐴 ) = ( 𝑖 ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) 𝑟 ) ∧ ( 𝑆 ‘ 𝐵 ) = ( 𝑗 ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) 𝑠 ) ) ) ) ∧ ¬ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) = ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) → ( 𝑟 ∈ ( 𝐼 × 2o ) ∧ 𝑠 ∈ ( 𝐼 × 2o ) ) )
124 123 simpld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) ) ) ∧ ( ( 𝑟 ∈ ( 𝐼 × 2o ) ∧ 𝑠 ∈ ( 𝐼 × 2o ) ) ∧ ( ( 𝑆 ‘ 𝐴 ) = ( 𝑖 ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) 𝑟 ) ∧ ( 𝑆 ‘ 𝐵 ) = ( 𝑗 ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) 𝑠 ) ) ) ) ∧ ¬ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) = ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) → 𝑟 ∈ ( 𝐼 × 2o ) )
125 123 simprd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) ) ) ∧ ( ( 𝑟 ∈ ( 𝐼 × 2o ) ∧ 𝑠 ∈ ( 𝐼 × 2o ) ) ∧ ( ( 𝑆 ‘ 𝐴 ) = ( 𝑖 ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) 𝑟 ) ∧ ( 𝑆 ‘ 𝐵 ) = ( 𝑗 ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) 𝑠 ) ) ) ) ∧ ¬ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) = ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) → 𝑠 ∈ ( 𝐼 × 2o ) )
126 simplrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) ) ) ∧ ( ( 𝑟 ∈ ( 𝐼 × 2o ) ∧ 𝑠 ∈ ( 𝐼 × 2o ) ) ∧ ( ( 𝑆 ‘ 𝐴 ) = ( 𝑖 ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) 𝑟 ) ∧ ( 𝑆 ‘ 𝐵 ) = ( 𝑗 ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) 𝑠 ) ) ) ) ∧ ¬ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) = ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) → ( ( 𝑆 ‘ 𝐴 ) = ( 𝑖 ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) 𝑟 ) ∧ ( 𝑆 ‘ 𝐵 ) = ( 𝑗 ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) 𝑠 ) ) )
127 126 simpld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) ) ) ∧ ( ( 𝑟 ∈ ( 𝐼 × 2o ) ∧ 𝑠 ∈ ( 𝐼 × 2o ) ) ∧ ( ( 𝑆 ‘ 𝐴 ) = ( 𝑖 ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) 𝑟 ) ∧ ( 𝑆 ‘ 𝐵 ) = ( 𝑗 ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) 𝑠 ) ) ) ) ∧ ¬ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) = ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) → ( 𝑆 ‘ 𝐴 ) = ( 𝑖 ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) 𝑟 ) )
128 126 simprd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) ) ) ∧ ( ( 𝑟 ∈ ( 𝐼 × 2o ) ∧ 𝑠 ∈ ( 𝐼 × 2o ) ) ∧ ( ( 𝑆 ‘ 𝐴 ) = ( 𝑖 ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) 𝑟 ) ∧ ( 𝑆 ‘ 𝐵 ) = ( 𝑗 ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) 𝑠 ) ) ) ) ∧ ¬ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) = ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) → ( 𝑆 ‘ 𝐵 ) = ( 𝑗 ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) 𝑠 ) )
129 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) ) ) ∧ ( ( 𝑟 ∈ ( 𝐼 × 2o ) ∧ 𝑠 ∈ ( 𝐼 × 2o ) ) ∧ ( ( 𝑆 ‘ 𝐴 ) = ( 𝑖 ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) 𝑟 ) ∧ ( 𝑆 ‘ 𝐵 ) = ( 𝑗 ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) 𝑠 ) ) ) ) ∧ ¬ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) = ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) → ¬ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) = ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) )
130 1 2 3 4 5 6 113 114 115 116 117 118 119 121 122 124 125 127 128 129 efgredlemb ⊢ ¬ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) ) ) ∧ ( ( 𝑟 ∈ ( 𝐼 × 2o ) ∧ 𝑠 ∈ ( 𝐼 × 2o ) ) ∧ ( ( 𝑆 ‘ 𝐴 ) = ( 𝑖 ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) 𝑟 ) ∧ ( 𝑆 ‘ 𝐵 ) = ( 𝑗 ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) 𝑠 ) ) ) ) ∧ ¬ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) = ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) )
131 iman ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) ) ) ∧ ( ( 𝑟 ∈ ( 𝐼 × 2o ) ∧ 𝑠 ∈ ( 𝐼 × 2o ) ) ∧ ( ( 𝑆 ‘ 𝐴 ) = ( 𝑖 ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) 𝑟 ) ∧ ( 𝑆 ‘ 𝐵 ) = ( 𝑗 ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) 𝑠 ) ) ) ) → ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) = ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ↔ ¬ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) ) ) ∧ ( ( 𝑟 ∈ ( 𝐼 × 2o ) ∧ 𝑠 ∈ ( 𝐼 × 2o ) ) ∧ ( ( 𝑆 ‘ 𝐴 ) = ( 𝑖 ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) 𝑟 ) ∧ ( 𝑆 ‘ 𝐵 ) = ( 𝑗 ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) 𝑠 ) ) ) ) ∧ ¬ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) = ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) )
132 130 131 mpbir ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) ) ) ∧ ( ( 𝑟 ∈ ( 𝐼 × 2o ) ∧ 𝑠 ∈ ( 𝐼 × 2o ) ) ∧ ( ( 𝑆 ‘ 𝐴 ) = ( 𝑖 ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) 𝑟 ) ∧ ( 𝑆 ‘ 𝐵 ) = ( 𝑗 ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) 𝑠 ) ) ) ) → ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) = ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) )
133 132 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) ) ) ∧ ( 𝑟 ∈ ( 𝐼 × 2o ) ∧ 𝑠 ∈ ( 𝐼 × 2o ) ) ) → ( ( ( 𝑆 ‘ 𝐴 ) = ( 𝑖 ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) 𝑟 ) ∧ ( 𝑆 ‘ 𝐵 ) = ( 𝑗 ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) 𝑠 ) ) → ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) = ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) )
134 133 rexlimdvva ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) ) ) → ( ∃ 𝑟 ∈ ( 𝐼 × 2o ) ∃ 𝑠 ∈ ( 𝐼 × 2o ) ( ( 𝑆 ‘ 𝐴 ) = ( 𝑖 ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) 𝑟 ) ∧ ( 𝑆 ‘ 𝐵 ) = ( 𝑗 ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) 𝑠 ) ) → ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) = ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) )
135 112 134 syl5bir ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) ) ) → ( ( ∃ 𝑟 ∈ ( 𝐼 × 2o ) ( 𝑆 ‘ 𝐴 ) = ( 𝑖 ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) 𝑟 ) ∧ ∃ 𝑠 ∈ ( 𝐼 × 2o ) ( 𝑆 ‘ 𝐵 ) = ( 𝑗 ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) 𝑠 ) ) → ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) = ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) )
136 135 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑖 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) ∃ 𝑗 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) ( ∃ 𝑟 ∈ ( 𝐼 × 2o ) ( 𝑆 ‘ 𝐴 ) = ( 𝑖 ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) 𝑟 ) ∧ ∃ 𝑠 ∈ ( 𝐼 × 2o ) ( 𝑆 ‘ 𝐵 ) = ( 𝑗 ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) 𝑠 ) ) → ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) = ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) )
137 111 136 syl5bir ⊢ ( 𝜑 → ( ( ∃ 𝑖 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) ∃ 𝑟 ∈ ( 𝐼 × 2o ) ( 𝑆 ‘ 𝐴 ) = ( 𝑖 ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) 𝑟 ) ∧ ∃ 𝑗 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) ) ∃ 𝑠 ∈ ( 𝐼 × 2o ) ( 𝑆 ‘ 𝐵 ) = ( 𝑗 ( 𝑇 ‘ ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) 𝑠 ) ) → ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) = ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) ) )
138 84 110 137 mp2and ⊢ ( 𝜑 → ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) = ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) )
139 fvres ⊢ ( ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) → ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) = ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) )
140 85 94 139 3syl ⊢ ( 𝜑 → ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) = ( 𝐵 ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) )
141 138 70 140 3eqtr4d ⊢ ( 𝜑 → ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) = ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) )
142 fz1ssfz0 ⊢ ( 1 ... ( ♯ ‘ 𝐵 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝐵 ) )
143 98 nn0red ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℝ )
144 143 lem1d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐵 ) − 1 ) ≤ ( ♯ ‘ 𝐵 ) )
145 fznn ⊢ ( ( ♯ ‘ 𝐵 ) ∈ ℤ → ( ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ↔ ( ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ℕ ∧ ( ( ♯ ‘ 𝐵 ) − 1 ) ≤ ( ♯ ‘ 𝐵 ) ) ) )
146 99 145 syl ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ↔ ( ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ℕ ∧ ( ( ♯ ‘ 𝐵 ) − 1 ) ≤ ( ♯ ‘ 𝐵 ) ) ) )
147 85 144 146 mpbir2and ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) )
148 142 147 sselid ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐵 ) ) )
149 pfxres ⊢ ( ( 𝐵 ∈ Word 𝑊 ∧ ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐵 ) ) ) → ( 𝐵 prefix ( ( ♯ ‘ 𝐵 ) − 1 ) ) = ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) )
150 91 148 149 syl2anc ⊢ ( 𝜑 → ( 𝐵 prefix ( ( ♯ ‘ 𝐵 ) − 1 ) ) = ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) )
151 150 fveq2d ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐵 prefix ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) = ( ♯ ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) )
152 pfxlen ⊢ ( ( 𝐵 ∈ Word 𝑊 ∧ ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐵 ) ) ) → ( ♯ ‘ ( 𝐵 prefix ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) = ( ( ♯ ‘ 𝐵 ) − 1 ) )
153 91 148 152 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐵 prefix ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) = ( ( ♯ ‘ 𝐵 ) − 1 ) )
154 151 153 eqtr3d ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) = ( ( ♯ ‘ 𝐵 ) − 1 ) )
155 154 fvoveq1d ⊢ ( 𝜑 → ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ‘ ( ( ♯ ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) − 1 ) ) = ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ‘ ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ) )
156 141 67 155 3eqtr4d ⊢ ( 𝜑 → ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ ( ( ♯ ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) − 1 ) ) = ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ‘ ( ( ♯ ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) − 1 ) ) )
157 1 2 3 4 5 6 efgsres ⊢ ( ( 𝐵 ∈ dom 𝑆 ∧ ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ) → ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ∈ dom 𝑆 )
158 9 147 157 syl2anc ⊢ ( 𝜑 → ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ∈ dom 𝑆 )
159 1 2 3 4 5 6 efgsval ⊢ ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ∈ dom 𝑆 → ( 𝑆 ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) = ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ‘ ( ( ♯ ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) − 1 ) ) )
160 158 159 syl ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) = ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ‘ ( ( ♯ ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) − 1 ) ) )
161 156 58 160 3eqtr4d ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) = ( 𝑆 ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) )
162 fveq2 ⊢ ( 𝑎 = ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) → ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) )
163 162 fveq2d ⊢ ( 𝑎 = ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) → ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) = ( ♯ ‘ ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) ) )
164 163 breq1d ⊢ ( 𝑎 = ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) → ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) ↔ ( ♯ ‘ ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) ) )
165 162 eqeq1d ⊢ ( 𝑎 = ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) ↔ ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) = ( 𝑆 ‘ 𝑏 ) ) )
166 fveq1 ⊢ ( 𝑎 = ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) → ( 𝑎 ‘ 0 ) = ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ 0 ) )
167 166 eqeq1d ⊢ ( 𝑎 = ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) → ( ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ↔ ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ 0 ) = ( 𝑏 ‘ 0 ) ) )
168 165 167 imbi12d ⊢ ( 𝑎 = ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) → ( ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ↔ ( ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) = ( 𝑆 ‘ 𝑏 ) → ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) )
169 164 168 imbi12d ⊢ ( 𝑎 = ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) → ( ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ↔ ( ( ♯ ‘ ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) → ( ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) = ( 𝑆 ‘ 𝑏 ) → ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ) )
170 fveq2 ⊢ ( 𝑏 = ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → ( 𝑆 ‘ 𝑏 ) = ( 𝑆 ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) )
171 170 eqeq2d ⊢ ( 𝑏 = ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → ( ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) = ( 𝑆 ‘ 𝑏 ) ↔ ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) = ( 𝑆 ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) ) )
172 fveq1 ⊢ ( 𝑏 = ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → ( 𝑏 ‘ 0 ) = ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ‘ 0 ) )
173 172 eqeq2d ⊢ ( 𝑏 = ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → ( ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ 0 ) = ( 𝑏 ‘ 0 ) ↔ ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ 0 ) = ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ‘ 0 ) ) )
174 171 173 imbi12d ⊢ ( 𝑏 = ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → ( ( ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) = ( 𝑆 ‘ 𝑏 ) → ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ↔ ( ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) = ( 𝑆 ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) → ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ 0 ) = ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ‘ 0 ) ) ) )
175 174 imbi2d ⊢ ( 𝑏 = ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → ( ( ( ♯ ‘ ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) → ( ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) = ( 𝑆 ‘ 𝑏 ) → ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ↔ ( ( ♯ ‘ ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) → ( ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) = ( 𝑆 ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) → ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ 0 ) = ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ‘ 0 ) ) ) ) )
176 169 175 rspc2va ⊢ ( ( ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ∈ dom 𝑆 ∧ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ∈ dom 𝑆 ) ∧ ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ) → ( ( ♯ ‘ ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) → ( ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) = ( 𝑆 ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) → ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ 0 ) = ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ‘ 0 ) ) ) )
177 56 158 7 176 syl21anc ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) → ( ( 𝑆 ‘ ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ) = ( 𝑆 ‘ ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ) → ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ 0 ) = ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ‘ 0 ) ) ) )
178 77 161 177 mp2d ⊢ ( 𝜑 → ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ 0 ) = ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ‘ 0 ) )
179 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ↔ ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ℕ )
180 21 179 sylibr ⊢ ( 𝜑 → 0 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) )
181 180 fvresd ⊢ ( 𝜑 → ( ( 𝐴 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ) ‘ 0 ) = ( 𝐴 ‘ 0 ) )
182 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ↔ ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ℕ )
183 85 182 sylibr ⊢ ( 𝜑 → 0 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) )
184 183 fvresd ⊢ ( 𝜑 → ( ( 𝐵 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) ‘ 0 ) = ( 𝐵 ‘ 0 ) )
185 178 181 184 3eqtr3d ⊢ ( 𝜑 → ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) )
186 185 11 pm2.65i ⊢ ¬ 𝜑