| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 3orass 1089 | . . 3
⊢ ((𝐵 ≤ 𝐴 ∨ (♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0) ↔ (𝐵 ≤ 𝐴 ∨ ((♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0))) | 
| 2 |  | pm2.24 124 | . . . . 5
⊢ (𝐵 ≤ 𝐴 → (¬ 𝐵 ≤ 𝐴 → ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑊 substr 〈𝐴, 𝐵〉) = ∅))) | 
| 3 |  | swrdval 14682 | . . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑊 substr 〈𝐴, 𝐵〉) = if((𝐴..^𝐵) ⊆ dom 𝑊, (𝑥 ∈ (0..^(𝐵 − 𝐴)) ↦ (𝑊‘(𝑥 + 𝐴))), ∅)) | 
| 4 | 3 | ad2antrr 726 | . . . . . . . . 9
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0)) ∧ ¬ 𝐵 ≤ 𝐴) → (𝑊 substr 〈𝐴, 𝐵〉) = if((𝐴..^𝐵) ⊆ dom 𝑊, (𝑥 ∈ (0..^(𝐵 − 𝐴)) ↦ (𝑊‘(𝑥 + 𝐴))), ∅)) | 
| 5 |  | wrddm 14560 | . . . . . . . . . . . . 13
⊢ (𝑊 ∈ Word 𝑉 → dom 𝑊 = (0..^(♯‘𝑊))) | 
| 6 |  | lencl 14572 | . . . . . . . . . . . . 13
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈
ℕ0) | 
| 7 |  | 3anass 1094 | . . . . . . . . . . . . . . . . 17
⊢
(((♯‘𝑊)
∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ↔
((♯‘𝑊) ∈
ℕ0 ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ))) | 
| 8 |  | ssfzoulel 13800 | . . . . . . . . . . . . . . . . . 18
⊢
(((♯‘𝑊)
∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) →
(((♯‘𝑊) ≤
𝐴 ∨ 𝐵 ≤ 0) → ((𝐴..^𝐵) ⊆ (0..^(♯‘𝑊)) → 𝐵 ≤ 𝐴))) | 
| 9 | 8 | imp 406 | . . . . . . . . . . . . . . . . 17
⊢
((((♯‘𝑊)
∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0)) → ((𝐴..^𝐵) ⊆ (0..^(♯‘𝑊)) → 𝐵 ≤ 𝐴)) | 
| 10 | 7, 9 | sylanbr 582 | . . . . . . . . . . . . . . . 16
⊢
((((♯‘𝑊)
∈ ℕ0 ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) ∧
((♯‘𝑊) ≤
𝐴 ∨ 𝐵 ≤ 0)) → ((𝐴..^𝐵) ⊆ (0..^(♯‘𝑊)) → 𝐵 ≤ 𝐴)) | 
| 11 | 10 | con3dimp 408 | . . . . . . . . . . . . . . 15
⊢
(((((♯‘𝑊) ∈ ℕ0 ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) ∧
((♯‘𝑊) ≤
𝐴 ∨ 𝐵 ≤ 0)) ∧ ¬ 𝐵 ≤ 𝐴) → ¬ (𝐴..^𝐵) ⊆ (0..^(♯‘𝑊))) | 
| 12 |  | sseq2 4009 | . . . . . . . . . . . . . . . 16
⊢ (dom
𝑊 =
(0..^(♯‘𝑊))
→ ((𝐴..^𝐵) ⊆ dom 𝑊 ↔ (𝐴..^𝐵) ⊆ (0..^(♯‘𝑊)))) | 
| 13 | 12 | notbid 318 | . . . . . . . . . . . . . . 15
⊢ (dom
𝑊 =
(0..^(♯‘𝑊))
→ (¬ (𝐴..^𝐵) ⊆ dom 𝑊 ↔ ¬ (𝐴..^𝐵) ⊆ (0..^(♯‘𝑊)))) | 
| 14 | 11, 13 | imbitrrid 246 | . . . . . . . . . . . . . 14
⊢ (dom
𝑊 =
(0..^(♯‘𝑊))
→ (((((♯‘𝑊) ∈ ℕ0 ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) ∧
((♯‘𝑊) ≤
𝐴 ∨ 𝐵 ≤ 0)) ∧ ¬ 𝐵 ≤ 𝐴) → ¬ (𝐴..^𝐵) ⊆ dom 𝑊)) | 
| 15 | 14 | exp5j 445 | . . . . . . . . . . . . 13
⊢ (dom
𝑊 =
(0..^(♯‘𝑊))
→ ((♯‘𝑊)
∈ ℕ0 → ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) →
(((♯‘𝑊) ≤
𝐴 ∨ 𝐵 ≤ 0) → (¬ 𝐵 ≤ 𝐴 → ¬ (𝐴..^𝐵) ⊆ dom 𝑊))))) | 
| 16 | 5, 6, 15 | sylc 65 | . . . . . . . . . . . 12
⊢ (𝑊 ∈ Word 𝑉 → ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) →
(((♯‘𝑊) ≤
𝐴 ∨ 𝐵 ≤ 0) → (¬ 𝐵 ≤ 𝐴 → ¬ (𝐴..^𝐵) ⊆ dom 𝑊)))) | 
| 17 | 16 | 3impib 1116 | . . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) →
(((♯‘𝑊) ≤
𝐴 ∨ 𝐵 ≤ 0) → (¬ 𝐵 ≤ 𝐴 → ¬ (𝐴..^𝐵) ⊆ dom 𝑊))) | 
| 18 | 17 | imp31 417 | . . . . . . . . . 10
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0)) ∧ ¬ 𝐵 ≤ 𝐴) → ¬ (𝐴..^𝐵) ⊆ dom 𝑊) | 
| 19 | 18 | iffalsed 4535 | . . . . . . . . 9
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0)) ∧ ¬ 𝐵 ≤ 𝐴) → if((𝐴..^𝐵) ⊆ dom 𝑊, (𝑥 ∈ (0..^(𝐵 − 𝐴)) ↦ (𝑊‘(𝑥 + 𝐴))), ∅) = ∅) | 
| 20 | 4, 19 | eqtrd 2776 | . . . . . . . 8
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0)) ∧ ¬ 𝐵 ≤ 𝐴) → (𝑊 substr 〈𝐴, 𝐵〉) = ∅) | 
| 21 | 20 | ex 412 | . . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0)) → (¬ 𝐵 ≤ 𝐴 → (𝑊 substr 〈𝐴, 𝐵〉) = ∅)) | 
| 22 | 21 | expcom 413 | . . . . . 6
⊢
(((♯‘𝑊)
≤ 𝐴 ∨ 𝐵 ≤ 0) → ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (¬ 𝐵 ≤ 𝐴 → (𝑊 substr 〈𝐴, 𝐵〉) = ∅))) | 
| 23 | 22 | com23 86 | . . . . 5
⊢
(((♯‘𝑊)
≤ 𝐴 ∨ 𝐵 ≤ 0) → (¬ 𝐵 ≤ 𝐴 → ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑊 substr 〈𝐴, 𝐵〉) = ∅))) | 
| 24 | 2, 23 | jaoi 857 | . . . 4
⊢ ((𝐵 ≤ 𝐴 ∨ ((♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0)) → (¬ 𝐵 ≤ 𝐴 → ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑊 substr 〈𝐴, 𝐵〉) = ∅))) | 
| 25 |  | swrdlend 14692 | . . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐵 ≤ 𝐴 → (𝑊 substr 〈𝐴, 𝐵〉) = ∅)) | 
| 26 | 25 | com12 32 | . . . 4
⊢ (𝐵 ≤ 𝐴 → ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑊 substr 〈𝐴, 𝐵〉) = ∅)) | 
| 27 | 24, 26 | pm2.61d2 181 | . . 3
⊢ ((𝐵 ≤ 𝐴 ∨ ((♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0)) → ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑊 substr 〈𝐴, 𝐵〉) = ∅)) | 
| 28 | 1, 27 | sylbi 217 | . 2
⊢ ((𝐵 ≤ 𝐴 ∨ (♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0) → ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑊 substr 〈𝐴, 𝐵〉) = ∅)) | 
| 29 | 28 | com12 32 | 1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐵 ≤ 𝐴 ∨ (♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0) → (𝑊 substr 〈𝐴, 𝐵〉) = ∅)) |