| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | efgval.w | . . . . . . . . . 10
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2o)) | 
| 2 |  | fviss 6986 | . . . . . . . . . 10
⊢ ( I
‘Word (𝐼 ×
2o)) ⊆ Word (𝐼 × 2o) | 
| 3 | 1, 2 | eqsstri 4030 | . . . . . . . . 9
⊢ 𝑊 ⊆ Word (𝐼 × 2o) | 
| 4 |  | efgredlem.2 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ dom 𝑆) | 
| 5 |  | efgval.r | . . . . . . . . . . . . . . 15
⊢  ∼ = (
~FG ‘𝐼) | 
| 6 |  | efgval2.m | . . . . . . . . . . . . . . 15
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉) | 
| 7 |  | efgval2.t | . . . . . . . . . . . . . . 15
⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) | 
| 8 |  | efgred.d | . . . . . . . . . . . . . . 15
⊢ 𝐷 = (𝑊 ∖ ∪
𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) | 
| 9 |  | efgred.s | . . . . . . . . . . . . . . 15
⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈
(1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1))) | 
| 10 | 1, 5, 6, 7, 8, 9 | efgsdm 19748 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ dom 𝑆 ↔ (𝐴 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝐴‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(♯‘𝐴))(𝐴‘𝑖) ∈ ran (𝑇‘(𝐴‘(𝑖 − 1))))) | 
| 11 | 10 | simp1bi 1146 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ dom 𝑆 → 𝐴 ∈ (Word 𝑊 ∖ {∅})) | 
| 12 | 4, 11 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ (Word 𝑊 ∖ {∅})) | 
| 13 | 12 | eldifad 3963 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ Word 𝑊) | 
| 14 |  | wrdf 14557 | . . . . . . . . . . 11
⊢ (𝐴 ∈ Word 𝑊 → 𝐴:(0..^(♯‘𝐴))⟶𝑊) | 
| 15 | 13, 14 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝐴:(0..^(♯‘𝐴))⟶𝑊) | 
| 16 |  | efgredlem.1 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < (♯‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) | 
| 17 |  | efgredlem.3 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ∈ dom 𝑆) | 
| 18 |  | efgredlem.4 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑆‘𝐴) = (𝑆‘𝐵)) | 
| 19 |  | efgredlem.5 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ¬ (𝐴‘0) = (𝐵‘0)) | 
| 20 | 1, 5, 6, 7, 8, 9, 16, 4, 17, 18, 19 | efgredlema 19758 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((♯‘𝐴) − 1) ∈ ℕ
∧ ((♯‘𝐵)
− 1) ∈ ℕ)) | 
| 21 | 20 | simpld 494 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((♯‘𝐴) − 1) ∈
ℕ) | 
| 22 |  | nnm1nn0 12567 | . . . . . . . . . . . . 13
⊢
(((♯‘𝐴)
− 1) ∈ ℕ → (((♯‘𝐴) − 1) − 1) ∈
ℕ0) | 
| 23 | 21, 22 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → (((♯‘𝐴) − 1) − 1) ∈
ℕ0) | 
| 24 | 21 | nnred 12281 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((♯‘𝐴) − 1) ∈
ℝ) | 
| 25 | 24 | lem1d 12201 | . . . . . . . . . . . 12
⊢ (𝜑 → (((♯‘𝐴) − 1) − 1) ≤
((♯‘𝐴) −
1)) | 
| 26 |  | eldifsni 4790 | . . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ (Word 𝑊 ∖ {∅}) → 𝐴 ≠ ∅) | 
| 27 | 4, 11, 26 | 3syl 18 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ≠ ∅) | 
| 28 |  | wrdfin 14570 | . . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ Word 𝑊 → 𝐴 ∈ Fin) | 
| 29 |  | hashnncl 14405 | . . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ Fin →
((♯‘𝐴) ∈
ℕ ↔ 𝐴 ≠
∅)) | 
| 30 | 13, 28, 29 | 3syl 18 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((♯‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅)) | 
| 31 | 27, 30 | mpbird 257 | . . . . . . . . . . . . 13
⊢ (𝜑 → (♯‘𝐴) ∈
ℕ) | 
| 32 |  | nnm1nn0 12567 | . . . . . . . . . . . . 13
⊢
((♯‘𝐴)
∈ ℕ → ((♯‘𝐴) − 1) ∈
ℕ0) | 
| 33 |  | fznn0 13659 | . . . . . . . . . . . . 13
⊢
(((♯‘𝐴)
− 1) ∈ ℕ0 → ((((♯‘𝐴) − 1) − 1) ∈
(0...((♯‘𝐴)
− 1)) ↔ ((((♯‘𝐴) − 1) − 1) ∈
ℕ0 ∧ (((♯‘𝐴) − 1) − 1) ≤
((♯‘𝐴) −
1)))) | 
| 34 | 31, 32, 33 | 3syl 18 | . . . . . . . . . . . 12
⊢ (𝜑 → ((((♯‘𝐴) − 1) − 1) ∈
(0...((♯‘𝐴)
− 1)) ↔ ((((♯‘𝐴) − 1) − 1) ∈
ℕ0 ∧ (((♯‘𝐴) − 1) − 1) ≤
((♯‘𝐴) −
1)))) | 
| 35 | 23, 25, 34 | mpbir2and 713 | . . . . . . . . . . 11
⊢ (𝜑 → (((♯‘𝐴) − 1) − 1) ∈
(0...((♯‘𝐴)
− 1))) | 
| 36 |  | lencl 14571 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ Word 𝑊 → (♯‘𝐴) ∈
ℕ0) | 
| 37 | 13, 36 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (♯‘𝐴) ∈
ℕ0) | 
| 38 | 37 | nn0zd 12639 | . . . . . . . . . . . 12
⊢ (𝜑 → (♯‘𝐴) ∈
ℤ) | 
| 39 |  | fzoval 13700 | . . . . . . . . . . . 12
⊢
((♯‘𝐴)
∈ ℤ → (0..^(♯‘𝐴)) = (0...((♯‘𝐴) − 1))) | 
| 40 | 38, 39 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (0..^(♯‘𝐴)) = (0...((♯‘𝐴) − 1))) | 
| 41 | 35, 40 | eleqtrrd 2844 | . . . . . . . . . 10
⊢ (𝜑 → (((♯‘𝐴) − 1) − 1) ∈
(0..^(♯‘𝐴))) | 
| 42 | 15, 41 | ffvelcdmd 7105 | . . . . . . . . 9
⊢ (𝜑 → (𝐴‘(((♯‘𝐴) − 1) − 1)) ∈ 𝑊) | 
| 43 | 3, 42 | sselid 3981 | . . . . . . . 8
⊢ (𝜑 → (𝐴‘(((♯‘𝐴) − 1) − 1)) ∈ Word (𝐼 ×
2o)) | 
| 44 |  | lencl 14571 | . . . . . . . 8
⊢ ((𝐴‘(((♯‘𝐴) − 1) − 1)) ∈
Word (𝐼 ×
2o) → (♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) ∈
ℕ0) | 
| 45 | 43, 44 | syl 17 | . . . . . . 7
⊢ (𝜑 → (♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) ∈
ℕ0) | 
| 46 | 45 | nn0red 12588 | . . . . . 6
⊢ (𝜑 → (♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) ∈
ℝ) | 
| 47 |  | 2rp 13039 | . . . . . 6
⊢ 2 ∈
ℝ+ | 
| 48 |  | ltaddrp 13072 | . . . . . 6
⊢
(((♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) ∈ ℝ
∧ 2 ∈ ℝ+) → (♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) <
((♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) +
2)) | 
| 49 | 46, 47, 48 | sylancl 586 | . . . . 5
⊢ (𝜑 → (♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) <
((♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) +
2)) | 
| 50 | 37 | nn0red 12588 | . . . . . . . . . . 11
⊢ (𝜑 → (♯‘𝐴) ∈
ℝ) | 
| 51 | 50 | lem1d 12201 | . . . . . . . . . 10
⊢ (𝜑 → ((♯‘𝐴) − 1) ≤
(♯‘𝐴)) | 
| 52 |  | fznn 13632 | . . . . . . . . . . 11
⊢
((♯‘𝐴)
∈ ℤ → (((♯‘𝐴) − 1) ∈
(1...(♯‘𝐴))
↔ (((♯‘𝐴)
− 1) ∈ ℕ ∧ ((♯‘𝐴) − 1) ≤ (♯‘𝐴)))) | 
| 53 | 38, 52 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (((♯‘𝐴) − 1) ∈
(1...(♯‘𝐴))
↔ (((♯‘𝐴)
− 1) ∈ ℕ ∧ ((♯‘𝐴) − 1) ≤ (♯‘𝐴)))) | 
| 54 | 21, 51, 53 | mpbir2and 713 | . . . . . . . . 9
⊢ (𝜑 → ((♯‘𝐴) − 1) ∈
(1...(♯‘𝐴))) | 
| 55 | 1, 5, 6, 7, 8, 9 | efgsres 19756 | . . . . . . . . 9
⊢ ((𝐴 ∈ dom 𝑆 ∧ ((♯‘𝐴) − 1) ∈
(1...(♯‘𝐴)))
→ (𝐴 ↾
(0..^((♯‘𝐴)
− 1))) ∈ dom 𝑆) | 
| 56 | 4, 54, 55 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (𝐴 ↾ (0..^((♯‘𝐴) − 1))) ∈ dom 𝑆) | 
| 57 | 1, 5, 6, 7, 8, 9 | efgsval 19749 | . . . . . . . 8
⊢ ((𝐴 ↾
(0..^((♯‘𝐴)
− 1))) ∈ dom 𝑆
→ (𝑆‘(𝐴 ↾
(0..^((♯‘𝐴)
− 1)))) = ((𝐴 ↾
(0..^((♯‘𝐴)
− 1)))‘((♯‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) −
1))) | 
| 58 | 56, 57 | syl 17 | . . . . . . 7
⊢ (𝜑 → (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = ((𝐴 ↾
(0..^((♯‘𝐴)
− 1)))‘((♯‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) −
1))) | 
| 59 |  | fz1ssfz0 13663 | . . . . . . . . . . . 12
⊢
(1...(♯‘𝐴)) ⊆ (0...(♯‘𝐴)) | 
| 60 | 59, 54 | sselid 3981 | . . . . . . . . . . 11
⊢ (𝜑 → ((♯‘𝐴) − 1) ∈
(0...(♯‘𝐴))) | 
| 61 |  | pfxres 14717 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ Word 𝑊 ∧ ((♯‘𝐴) − 1) ∈
(0...(♯‘𝐴)))
→ (𝐴 prefix
((♯‘𝐴) −
1)) = (𝐴 ↾
(0..^((♯‘𝐴)
− 1)))) | 
| 62 | 13, 60, 61 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 → (𝐴 prefix ((♯‘𝐴) − 1)) = (𝐴 ↾ (0..^((♯‘𝐴) − 1)))) | 
| 63 | 62 | fveq2d 6910 | . . . . . . . . 9
⊢ (𝜑 → (♯‘(𝐴 prefix ((♯‘𝐴) − 1))) =
(♯‘(𝐴 ↾
(0..^((♯‘𝐴)
− 1))))) | 
| 64 |  | pfxlen 14721 | . . . . . . . . . 10
⊢ ((𝐴 ∈ Word 𝑊 ∧ ((♯‘𝐴) − 1) ∈
(0...(♯‘𝐴)))
→ (♯‘(𝐴
prefix ((♯‘𝐴)
− 1))) = ((♯‘𝐴) − 1)) | 
| 65 | 13, 60, 64 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (♯‘(𝐴 prefix ((♯‘𝐴) − 1))) =
((♯‘𝐴) −
1)) | 
| 66 | 63, 65 | eqtr3d 2779 | . . . . . . . 8
⊢ (𝜑 → (♯‘(𝐴 ↾
(0..^((♯‘𝐴)
− 1)))) = ((♯‘𝐴) − 1)) | 
| 67 | 66 | fvoveq1d 7453 | . . . . . . 7
⊢ (𝜑 → ((𝐴 ↾ (0..^((♯‘𝐴) −
1)))‘((♯‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) − 1)) =
((𝐴 ↾
(0..^((♯‘𝐴)
− 1)))‘(((♯‘𝐴) − 1) − 1))) | 
| 68 |  | fzo0end 13797 | . . . . . . . 8
⊢
(((♯‘𝐴)
− 1) ∈ ℕ → (((♯‘𝐴) − 1) − 1) ∈
(0..^((♯‘𝐴)
− 1))) | 
| 69 |  | fvres 6925 | . . . . . . . 8
⊢
((((♯‘𝐴)
− 1) − 1) ∈ (0..^((♯‘𝐴) − 1)) → ((𝐴 ↾ (0..^((♯‘𝐴) −
1)))‘(((♯‘𝐴) − 1) − 1)) = (𝐴‘(((♯‘𝐴) − 1) −
1))) | 
| 70 | 21, 68, 69 | 3syl 18 | . . . . . . 7
⊢ (𝜑 → ((𝐴 ↾ (0..^((♯‘𝐴) −
1)))‘(((♯‘𝐴) − 1) − 1)) = (𝐴‘(((♯‘𝐴) − 1) −
1))) | 
| 71 | 58, 67, 70 | 3eqtrd 2781 | . . . . . 6
⊢ (𝜑 → (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝐴‘(((♯‘𝐴) − 1) −
1))) | 
| 72 | 71 | fveq2d 6910 | . . . . 5
⊢ (𝜑 → (♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) =
(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) | 
| 73 | 1, 5, 6, 7, 8, 9 | efgsdmi 19750 | . . . . . . 7
⊢ ((𝐴 ∈ dom 𝑆 ∧ ((♯‘𝐴) − 1) ∈ ℕ) → (𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) | 
| 74 | 4, 21, 73 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → (𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) | 
| 75 | 1, 5, 6, 7 | efgtlen 19744 | . . . . . 6
⊢ (((𝐴‘(((♯‘𝐴) − 1) − 1)) ∈
𝑊 ∧ (𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) →
(♯‘(𝑆‘𝐴)) = ((♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) +
2)) | 
| 76 | 42, 74, 75 | syl2anc 584 | . . . . 5
⊢ (𝜑 → (♯‘(𝑆‘𝐴)) = ((♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) +
2)) | 
| 77 | 49, 72, 76 | 3brtr4d 5175 | . . . 4
⊢ (𝜑 → (♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) <
(♯‘(𝑆‘𝐴))) | 
| 78 | 1, 5, 6, 7 | efgtf 19740 | . . . . . . . . . . . 12
⊢ ((𝐴‘(((♯‘𝐴) − 1) − 1)) ∈
𝑊 → ((𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))) = (𝑎 ∈
(0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))), 𝑏 ∈ (𝐼 × 2o) ↦ ((𝐴‘(((♯‘𝐴) − 1) − 1)) splice
〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) ∧ (𝑇‘(𝐴‘(((♯‘𝐴) − 1) −
1))):((0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) × (𝐼 ×
2o))⟶𝑊)) | 
| 79 | 42, 78 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))) = (𝑎 ∈
(0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))), 𝑏 ∈ (𝐼 × 2o) ↦ ((𝐴‘(((♯‘𝐴) − 1) − 1)) splice
〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) ∧ (𝑇‘(𝐴‘(((♯‘𝐴) − 1) −
1))):((0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) × (𝐼 ×
2o))⟶𝑊)) | 
| 80 | 79 | simprd 495 | . . . . . . . . . 10
⊢ (𝜑 → (𝑇‘(𝐴‘(((♯‘𝐴) − 1) −
1))):((0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) × (𝐼 ×
2o))⟶𝑊) | 
| 81 |  | ffn 6736 | . . . . . . . . . 10
⊢ ((𝑇‘(𝐴‘(((♯‘𝐴) − 1) −
1))):((0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) × (𝐼 ×
2o))⟶𝑊
→ (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))) Fn
((0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) × (𝐼 ×
2o))) | 
| 82 |  | ovelrn 7609 | . . . . . . . . . 10
⊢ ((𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))) Fn
((0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) × (𝐼 × 2o)) →
((𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))) ↔
∃𝑖 ∈
(0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))))∃𝑟 ∈ (𝐼 × 2o)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟))) | 
| 83 | 80, 81, 82 | 3syl 18 | . . . . . . . . 9
⊢ (𝜑 → ((𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))) ↔
∃𝑖 ∈
(0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))))∃𝑟 ∈ (𝐼 × 2o)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟))) | 
| 84 | 74, 83 | mpbid 232 | . . . . . . . 8
⊢ (𝜑 → ∃𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) −
1))))∃𝑟 ∈ (𝐼 × 2o)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟)) | 
| 85 | 20 | simprd 495 | . . . . . . . . . 10
⊢ (𝜑 → ((♯‘𝐵) − 1) ∈
ℕ) | 
| 86 | 1, 5, 6, 7, 8, 9 | efgsdmi 19750 | . . . . . . . . . 10
⊢ ((𝐵 ∈ dom 𝑆 ∧ ((♯‘𝐵) − 1) ∈ ℕ) → (𝑆‘𝐵) ∈ ran (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))) | 
| 87 | 17, 85, 86 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (𝑆‘𝐵) ∈ ran (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))) | 
| 88 | 1, 5, 6, 7, 8, 9 | efgsdm 19748 | . . . . . . . . . . . . . . . . 17
⊢ (𝐵 ∈ dom 𝑆 ↔ (𝐵 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝐵‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(♯‘𝐵))(𝐵‘𝑖) ∈ ran (𝑇‘(𝐵‘(𝑖 − 1))))) | 
| 89 | 88 | simp1bi 1146 | . . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ dom 𝑆 → 𝐵 ∈ (Word 𝑊 ∖ {∅})) | 
| 90 | 17, 89 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ∈ (Word 𝑊 ∖ {∅})) | 
| 91 | 90 | eldifad 3963 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∈ Word 𝑊) | 
| 92 |  | wrdf 14557 | . . . . . . . . . . . . . 14
⊢ (𝐵 ∈ Word 𝑊 → 𝐵:(0..^(♯‘𝐵))⟶𝑊) | 
| 93 | 91, 92 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵:(0..^(♯‘𝐵))⟶𝑊) | 
| 94 |  | fzo0end 13797 | . . . . . . . . . . . . . . 15
⊢
(((♯‘𝐵)
− 1) ∈ ℕ → (((♯‘𝐵) − 1) − 1) ∈
(0..^((♯‘𝐵)
− 1))) | 
| 95 |  | elfzofz 13715 | . . . . . . . . . . . . . . 15
⊢
((((♯‘𝐵)
− 1) − 1) ∈ (0..^((♯‘𝐵) − 1)) → (((♯‘𝐵) − 1) − 1) ∈
(0...((♯‘𝐵)
− 1))) | 
| 96 | 85, 94, 95 | 3syl 18 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((♯‘𝐵) − 1) − 1) ∈
(0...((♯‘𝐵)
− 1))) | 
| 97 |  | lencl 14571 | . . . . . . . . . . . . . . . . 17
⊢ (𝐵 ∈ Word 𝑊 → (♯‘𝐵) ∈
ℕ0) | 
| 98 | 91, 97 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (♯‘𝐵) ∈
ℕ0) | 
| 99 | 98 | nn0zd 12639 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (♯‘𝐵) ∈
ℤ) | 
| 100 |  | fzoval 13700 | . . . . . . . . . . . . . . 15
⊢
((♯‘𝐵)
∈ ℤ → (0..^(♯‘𝐵)) = (0...((♯‘𝐵) − 1))) | 
| 101 | 99, 100 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (0..^(♯‘𝐵)) = (0...((♯‘𝐵) − 1))) | 
| 102 | 96, 101 | eleqtrrd 2844 | . . . . . . . . . . . . 13
⊢ (𝜑 → (((♯‘𝐵) − 1) − 1) ∈
(0..^(♯‘𝐵))) | 
| 103 | 93, 102 | ffvelcdmd 7105 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐵‘(((♯‘𝐵) − 1) − 1)) ∈ 𝑊) | 
| 104 | 1, 5, 6, 7 | efgtf 19740 | . . . . . . . . . . . 12
⊢ ((𝐵‘(((♯‘𝐵) − 1) − 1)) ∈
𝑊 → ((𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))) = (𝑎 ∈
(0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))), 𝑏 ∈ (𝐼 × 2o) ↦ ((𝐵‘(((♯‘𝐵) − 1) − 1)) splice
〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) ∧ (𝑇‘(𝐵‘(((♯‘𝐵) − 1) −
1))):((0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))) × (𝐼 ×
2o))⟶𝑊)) | 
| 105 | 103, 104 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))) = (𝑎 ∈
(0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))), 𝑏 ∈ (𝐼 × 2o) ↦ ((𝐵‘(((♯‘𝐵) − 1) − 1)) splice
〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) ∧ (𝑇‘(𝐵‘(((♯‘𝐵) − 1) −
1))):((0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))) × (𝐼 ×
2o))⟶𝑊)) | 
| 106 | 105 | simprd 495 | . . . . . . . . . 10
⊢ (𝜑 → (𝑇‘(𝐵‘(((♯‘𝐵) − 1) −
1))):((0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))) × (𝐼 ×
2o))⟶𝑊) | 
| 107 |  | ffn 6736 | . . . . . . . . . 10
⊢ ((𝑇‘(𝐵‘(((♯‘𝐵) − 1) −
1))):((0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))) × (𝐼 ×
2o))⟶𝑊
→ (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))) Fn
((0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))) × (𝐼 ×
2o))) | 
| 108 |  | ovelrn 7609 | . . . . . . . . . 10
⊢ ((𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))) Fn
((0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))) × (𝐼 × 2o)) →
((𝑆‘𝐵) ∈ ran (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))) ↔
∃𝑗 ∈
(0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1))))∃𝑠 ∈ (𝐼 × 2o)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠))) | 
| 109 | 106, 107,
108 | 3syl 18 | . . . . . . . . 9
⊢ (𝜑 → ((𝑆‘𝐵) ∈ ran (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))) ↔
∃𝑗 ∈
(0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1))))∃𝑠 ∈ (𝐼 × 2o)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠))) | 
| 110 | 87, 109 | mpbid 232 | . . . . . . . 8
⊢ (𝜑 → ∃𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) −
1))))∃𝑠 ∈ (𝐼 × 2o)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)) | 
| 111 |  | reeanv 3229 | . . . . . . . . 9
⊢
(∃𝑖 ∈
(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 3229 | . . . . . . . . . . 11
⊢
(∃𝑟 ∈
(𝐼 ×
2o)∃𝑠
∈ (𝐼 ×
2o)((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)) ↔ (∃𝑟 ∈ (𝐼 × 2o)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ ∃𝑠 ∈ (𝐼 × 2o)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠))) | 
| 113 | 16 | ad3antrrr 730 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧
𝑗 ∈
(0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) →
∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < (♯‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) | 
| 114 | 4 | ad3antrrr 730 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧
𝑗 ∈
(0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) →
𝐴 ∈ dom 𝑆) | 
| 115 | 17 | ad3antrrr 730 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧
𝑗 ∈
(0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) →
𝐵 ∈ dom 𝑆) | 
| 116 | 18 | ad3antrrr 730 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧
𝑗 ∈
(0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) →
(𝑆‘𝐴) = (𝑆‘𝐵)) | 
| 117 | 19 | ad3antrrr 730 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧
𝑗 ∈
(0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) →
¬ (𝐴‘0) = (𝐵‘0)) | 
| 118 |  | eqid 2737 | . . . . . . . . . . . . . . 15
⊢
(((♯‘𝐴)
− 1) − 1) = (((♯‘𝐴) − 1) − 1) | 
| 119 |  | eqid 2737 | . . . . . . . . . . . . . . 15
⊢
(((♯‘𝐵)
− 1) − 1) = (((♯‘𝐵) − 1) − 1) | 
| 120 |  | simpllr 776 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑖 ∈ (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 494 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧
𝑗 ∈
(0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) →
𝑖 ∈
(0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))))) | 
| 122 | 120 | simprd 495 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧
𝑗 ∈
(0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) →
𝑗 ∈
(0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1))))) | 
| 123 |  | simplrl 777 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧
𝑗 ∈
(0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) →
(𝑟 ∈ (𝐼 × 2o) ∧
𝑠 ∈ (𝐼 × 2o))) | 
| 124 | 123 | simpld 494 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧
𝑗 ∈
(0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) →
𝑟 ∈ (𝐼 × 2o)) | 
| 125 | 123 | simprd 495 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧
𝑗 ∈
(0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) →
𝑠 ∈ (𝐼 × 2o)) | 
| 126 |  | simplrr 778 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧
𝑗 ∈
(0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) →
((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠))) | 
| 127 | 126 | simpld 494 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧
𝑗 ∈
(0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) →
(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟)) | 
| 128 | 126 | simprd 495 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧
𝑗 ∈
(0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) →
(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)) | 
| 129 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧
𝑗 ∈
(0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) →
¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) −
1))) | 
| 130 | 1, 5, 6, 7, 8, 9, 113, 114, 115, 116, 117, 118, 119, 121, 122, 124, 125, 127, 128, 129 | efgredlemb 19764 | . . . . . . . . . . . . . 14
⊢  ¬
(((𝜑 ∧ (𝑖 ∈
(0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈
(0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) −
1))) | 
| 131 |  | iman 401 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑖 ∈ (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 231 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧
𝑗 ∈
(0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o)) ∧ ((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) → (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) −
1))) | 
| 133 | 132 | expr 456 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧
𝑗 ∈
(0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ (𝑟 ∈ (𝐼 × 2o) ∧ 𝑠 ∈ (𝐼 × 2o))) → (((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)) → (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) −
1)))) | 
| 134 | 133 | rexlimdvva 3213 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧
𝑗 ∈
(0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) →
(∃𝑟 ∈ (𝐼 ×
2o)∃𝑠
∈ (𝐼 ×
2o)((𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)) → (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) −
1)))) | 
| 135 | 112, 134 | biimtrrid 243 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧
𝑗 ∈
(0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) →
((∃𝑟 ∈ (𝐼 × 2o)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ ∃𝑠 ∈ (𝐼 × 2o)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)) → (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) −
1)))) | 
| 136 | 135 | rexlimdvva 3213 | . . . . . . . . 9
⊢ (𝜑 → (∃𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) −
1))))∃𝑗 ∈
(0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1))))(∃𝑟 ∈ (𝐼 × 2o)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ ∃𝑠 ∈ (𝐼 × 2o)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)) → (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) −
1)))) | 
| 137 | 111, 136 | biimtrrid 243 | . . . . . . . 8
⊢ (𝜑 → ((∃𝑖 ∈
(0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))))∃𝑟 ∈ (𝐼 × 2o)(𝑆‘𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ ∃𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) −
1))))∃𝑠 ∈ (𝐼 × 2o)(𝑆‘𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)) → (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) −
1)))) | 
| 138 | 84, 110, 137 | mp2and 699 | . . . . . . 7
⊢ (𝜑 → (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) −
1))) | 
| 139 |  | fvres 6925 | . . . . . . . 8
⊢
((((♯‘𝐵)
− 1) − 1) ∈ (0..^((♯‘𝐵) − 1)) → ((𝐵 ↾ (0..^((♯‘𝐵) −
1)))‘(((♯‘𝐵) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) −
1))) | 
| 140 | 85, 94, 139 | 3syl 18 | . . . . . . 7
⊢ (𝜑 → ((𝐵 ↾ (0..^((♯‘𝐵) −
1)))‘(((♯‘𝐵) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) −
1))) | 
| 141 | 138, 70, 140 | 3eqtr4d 2787 | . . . . . 6
⊢ (𝜑 → ((𝐴 ↾ (0..^((♯‘𝐴) −
1)))‘(((♯‘𝐴) − 1) − 1)) = ((𝐵 ↾
(0..^((♯‘𝐵)
− 1)))‘(((♯‘𝐵) − 1) − 1))) | 
| 142 |  | fz1ssfz0 13663 | . . . . . . . . . . 11
⊢
(1...(♯‘𝐵)) ⊆ (0...(♯‘𝐵)) | 
| 143 | 98 | nn0red 12588 | . . . . . . . . . . . . 13
⊢ (𝜑 → (♯‘𝐵) ∈
ℝ) | 
| 144 | 143 | lem1d 12201 | . . . . . . . . . . . 12
⊢ (𝜑 → ((♯‘𝐵) − 1) ≤
(♯‘𝐵)) | 
| 145 |  | fznn 13632 | . . . . . . . . . . . . 13
⊢
((♯‘𝐵)
∈ ℤ → (((♯‘𝐵) − 1) ∈
(1...(♯‘𝐵))
↔ (((♯‘𝐵)
− 1) ∈ ℕ ∧ ((♯‘𝐵) − 1) ≤ (♯‘𝐵)))) | 
| 146 | 99, 145 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → (((♯‘𝐵) − 1) ∈
(1...(♯‘𝐵))
↔ (((♯‘𝐵)
− 1) ∈ ℕ ∧ ((♯‘𝐵) − 1) ≤ (♯‘𝐵)))) | 
| 147 | 85, 144, 146 | mpbir2and 713 | . . . . . . . . . . 11
⊢ (𝜑 → ((♯‘𝐵) − 1) ∈
(1...(♯‘𝐵))) | 
| 148 | 142, 147 | sselid 3981 | . . . . . . . . . 10
⊢ (𝜑 → ((♯‘𝐵) − 1) ∈
(0...(♯‘𝐵))) | 
| 149 |  | pfxres 14717 | . . . . . . . . . 10
⊢ ((𝐵 ∈ Word 𝑊 ∧ ((♯‘𝐵) − 1) ∈
(0...(♯‘𝐵)))
→ (𝐵 prefix
((♯‘𝐵) −
1)) = (𝐵 ↾
(0..^((♯‘𝐵)
− 1)))) | 
| 150 | 91, 148, 149 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (𝐵 prefix ((♯‘𝐵) − 1)) = (𝐵 ↾ (0..^((♯‘𝐵) − 1)))) | 
| 151 | 150 | fveq2d 6910 | . . . . . . . 8
⊢ (𝜑 → (♯‘(𝐵 prefix ((♯‘𝐵) − 1))) =
(♯‘(𝐵 ↾
(0..^((♯‘𝐵)
− 1))))) | 
| 152 |  | pfxlen 14721 | . . . . . . . . 9
⊢ ((𝐵 ∈ Word 𝑊 ∧ ((♯‘𝐵) − 1) ∈
(0...(♯‘𝐵)))
→ (♯‘(𝐵
prefix ((♯‘𝐵)
− 1))) = ((♯‘𝐵) − 1)) | 
| 153 | 91, 148, 152 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (♯‘(𝐵 prefix ((♯‘𝐵) − 1))) =
((♯‘𝐵) −
1)) | 
| 154 | 151, 153 | eqtr3d 2779 | . . . . . . 7
⊢ (𝜑 → (♯‘(𝐵 ↾
(0..^((♯‘𝐵)
− 1)))) = ((♯‘𝐵) − 1)) | 
| 155 | 154 | fvoveq1d 7453 | . . . . . 6
⊢ (𝜑 → ((𝐵 ↾ (0..^((♯‘𝐵) −
1)))‘((♯‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) − 1)) =
((𝐵 ↾
(0..^((♯‘𝐵)
− 1)))‘(((♯‘𝐵) − 1) − 1))) | 
| 156 | 141, 67, 155 | 3eqtr4d 2787 | . . . . 5
⊢ (𝜑 → ((𝐴 ↾ (0..^((♯‘𝐴) −
1)))‘((♯‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) − 1)) =
((𝐵 ↾
(0..^((♯‘𝐵)
− 1)))‘((♯‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) −
1))) | 
| 157 | 1, 5, 6, 7, 8, 9 | efgsres 19756 | . . . . . . 7
⊢ ((𝐵 ∈ dom 𝑆 ∧ ((♯‘𝐵) − 1) ∈
(1...(♯‘𝐵)))
→ (𝐵 ↾
(0..^((♯‘𝐵)
− 1))) ∈ dom 𝑆) | 
| 158 | 17, 147, 157 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → (𝐵 ↾ (0..^((♯‘𝐵) − 1))) ∈ dom 𝑆) | 
| 159 | 1, 5, 6, 7, 8, 9 | efgsval 19749 | . . . . . 6
⊢ ((𝐵 ↾
(0..^((♯‘𝐵)
− 1))) ∈ dom 𝑆
→ (𝑆‘(𝐵 ↾
(0..^((♯‘𝐵)
− 1)))) = ((𝐵 ↾
(0..^((♯‘𝐵)
− 1)))‘((♯‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) −
1))) | 
| 160 | 158, 159 | syl 17 | . . . . 5
⊢ (𝜑 → (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) = ((𝐵 ↾
(0..^((♯‘𝐵)
− 1)))‘((♯‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) −
1))) | 
| 161 | 156, 58, 160 | 3eqtr4d 2787 | . . . 4
⊢ (𝜑 → (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) −
1))))) | 
| 162 |  | fveq2 6906 | . . . . . . . . 9
⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → (𝑆‘𝑎) = (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) −
1))))) | 
| 163 | 162 | fveq2d 6910 | . . . . . . . 8
⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) →
(♯‘(𝑆‘𝑎)) = (♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) −
1)))))) | 
| 164 | 163 | breq1d 5153 | . . . . . . 7
⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) →
((♯‘(𝑆‘𝑎)) < (♯‘(𝑆‘𝐴)) ↔ (♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) <
(♯‘(𝑆‘𝐴)))) | 
| 165 | 162 | eqeq1d 2739 | . . . . . . . 8
⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → ((𝑆‘𝑎) = (𝑆‘𝑏) ↔ (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘𝑏))) | 
| 166 |  | fveq1 6905 | . . . . . . . . 9
⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → (𝑎‘0) = ((𝐴 ↾ (0..^((♯‘𝐴) −
1)))‘0)) | 
| 167 | 166 | eqeq1d 2739 | . . . . . . . 8
⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → ((𝑎‘0) = (𝑏‘0) ↔ ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = (𝑏‘0))) | 
| 168 | 165, 167 | imbi12d 344 | . . . . . . 7
⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → (((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)) ↔ ((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘𝑏) → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = (𝑏‘0)))) | 
| 169 | 164, 168 | imbi12d 344 | . . . . . 6
⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) →
(((♯‘(𝑆‘𝑎)) < (♯‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ ((♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) <
(♯‘(𝑆‘𝐴)) → ((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘𝑏) → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = (𝑏‘0))))) | 
| 170 |  | fveq2 6906 | . . . . . . . . 9
⊢ (𝑏 = (𝐵 ↾ (0..^((♯‘𝐵) − 1))) → (𝑆‘𝑏) = (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) −
1))))) | 
| 171 | 170 | eqeq2d 2748 | . . . . . . . 8
⊢ (𝑏 = (𝐵 ↾ (0..^((♯‘𝐵) − 1))) → ((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘𝑏) ↔ (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) −
1)))))) | 
| 172 |  | fveq1 6905 | . . . . . . . . 9
⊢ (𝑏 = (𝐵 ↾ (0..^((♯‘𝐵) − 1))) → (𝑏‘0) = ((𝐵 ↾ (0..^((♯‘𝐵) −
1)))‘0)) | 
| 173 | 172 | eqeq2d 2748 | . . . . . . . 8
⊢ (𝑏 = (𝐵 ↾ (0..^((♯‘𝐵) − 1))) → (((𝐴 ↾
(0..^((♯‘𝐴)
− 1)))‘0) = (𝑏‘0) ↔ ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) =
((𝐵 ↾
(0..^((♯‘𝐵)
− 1)))‘0))) | 
| 174 | 171, 173 | imbi12d 344 | . . . . . . 7
⊢ (𝑏 = (𝐵 ↾ (0..^((♯‘𝐵) − 1))) → (((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘𝑏) → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = (𝑏‘0)) ↔ ((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) → ((𝐴 ↾
(0..^((♯‘𝐴)
− 1)))‘0) = ((𝐵
↾ (0..^((♯‘𝐵) − 1)))‘0)))) | 
| 175 | 174 | imbi2d 340 | . . . . . 6
⊢ (𝑏 = (𝐵 ↾ (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 3634 | . . . . 5
⊢ ((((𝐴 ↾
(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, 16, 176 | syl21anc 838 | . . . 4
⊢ (𝜑 → ((♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) <
(♯‘(𝑆‘𝐴)) → ((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) → ((𝐴 ↾
(0..^((♯‘𝐴)
− 1)))‘0) = ((𝐵
↾ (0..^((♯‘𝐵) − 1)))‘0)))) | 
| 178 | 77, 161, 177 | mp2d 49 | . . 3
⊢ (𝜑 → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) =
((𝐵 ↾
(0..^((♯‘𝐵)
− 1)))‘0)) | 
| 179 |  | lbfzo0 13739 | . . . . 5
⊢ (0 ∈
(0..^((♯‘𝐴)
− 1)) ↔ ((♯‘𝐴) − 1) ∈
ℕ) | 
| 180 | 21, 179 | sylibr 234 | . . . 4
⊢ (𝜑 → 0 ∈
(0..^((♯‘𝐴)
− 1))) | 
| 181 | 180 | fvresd 6926 | . . 3
⊢ (𝜑 → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = (𝐴‘0)) | 
| 182 |  | lbfzo0 13739 | . . . . 5
⊢ (0 ∈
(0..^((♯‘𝐵)
− 1)) ↔ ((♯‘𝐵) − 1) ∈
ℕ) | 
| 183 | 85, 182 | sylibr 234 | . . . 4
⊢ (𝜑 → 0 ∈
(0..^((♯‘𝐵)
− 1))) | 
| 184 | 183 | fvresd 6926 | . . 3
⊢ (𝜑 → ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0) = (𝐵‘0)) | 
| 185 | 178, 181,
184 | 3eqtr3d 2785 | . 2
⊢ (𝜑 → (𝐴‘0) = (𝐵‘0)) | 
| 186 | 185, 19 | pm2.65i 194 | 1
⊢  ¬
𝜑 |