Metamath Proof Explorer

Theorem swrdnd0

Description: The value of a subword operation for inproper arguments is the empty set. (Contributed by AV, 2-Dec-2022)

Ref Expression
Assertion swrdnd0 ( 𝑆 ∈ Word 𝑉 → ( ¬ ( 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 ianor ⊢ ( ¬ ( 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ↔ ( ¬ 𝐹 ∈ ( 0 ... 𝐿 ) ∨ ¬ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) )
2 3ianor ⊢ ( ¬ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝐹 ≤ 𝐿 ) ↔ ( ¬ 𝐹 ∈ ℕ0 ∨ ¬ 𝐿 ∈ ℕ0 ∨ ¬ 𝐹 ≤ 𝐿 ) )
3 elfz2nn0 ⊢ ( 𝐹 ∈ ( 0 ... 𝐿 ) ↔ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝐹 ≤ 𝐿 ) )
4 2 3 xchnxbir ⊢ ( ¬ 𝐹 ∈ ( 0 ... 𝐿 ) ↔ ( ¬ 𝐹 ∈ ℕ0 ∨ ¬ 𝐿 ∈ ℕ0 ∨ ¬ 𝐹 ≤ 𝐿 ) )
5 3ianor ⊢ ( ¬ ( 𝐿 ∈ ℕ0 ∧ ( ♯ ‘ 𝑆 ) ∈ ℕ0 ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) ↔ ( ¬ 𝐿 ∈ ℕ0 ∨ ¬ ( ♯ ‘ 𝑆 ) ∈ ℕ0 ∨ ¬ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) )
6 elfz2nn0 ⊢ ( 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ↔ ( 𝐿 ∈ ℕ0 ∧ ( ♯ ‘ 𝑆 ) ∈ ℕ0 ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) )
7 5 6 xchnxbir ⊢ ( ¬ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ↔ ( ¬ 𝐿 ∈ ℕ0 ∨ ¬ ( ♯ ‘ 𝑆 ) ∈ ℕ0 ∨ ¬ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) )
8 4 7 orbi12i ⊢ ( ( ¬ 𝐹 ∈ ( 0 ... 𝐿 ) ∨ ¬ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ↔ ( ( ¬ 𝐹 ∈ ℕ0 ∨ ¬ 𝐿 ∈ ℕ0 ∨ ¬ 𝐹 ≤ 𝐿 ) ∨ ( ¬ 𝐿 ∈ ℕ0 ∨ ¬ ( ♯ ‘ 𝑆 ) ∈ ℕ0 ∨ ¬ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) ) )
9 1 8 bitri ⊢ ( ¬ ( 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ↔ ( ( ¬ 𝐹 ∈ ℕ0 ∨ ¬ 𝐿 ∈ ℕ0 ∨ ¬ 𝐹 ≤ 𝐿 ) ∨ ( ¬ 𝐿 ∈ ℕ0 ∨ ¬ ( ♯ ‘ 𝑆 ) ∈ ℕ0 ∨ ¬ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) ) )
10 df-3or ⊢ ( ( ¬ 𝐹 ∈ ℕ0 ∨ ¬ 𝐿 ∈ ℕ0 ∨ ¬ 𝐹 ≤ 𝐿 ) ↔ ( ( ¬ 𝐹 ∈ ℕ0 ∨ ¬ 𝐿 ∈ ℕ0 ) ∨ ¬ 𝐹 ≤ 𝐿 ) )
11 ianor ⊢ ( ¬ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ↔ ( ¬ 𝐹 ∈ ℕ0 ∨ ¬ 𝐿 ∈ ℕ0 ) )
12 swrdnnn0nd ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ¬ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ )
13 12 expcom ⊢ ( ¬ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑆 ∈ Word 𝑉 → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) )
14 11 13 sylbir ⊢ ( ( ¬ 𝐹 ∈ ℕ0 ∨ ¬ 𝐿 ∈ ℕ0 ) → ( 𝑆 ∈ Word 𝑉 → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) )
15 anor ⊢ ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ↔ ¬ ( ¬ 𝐹 ∈ ℕ0 ∨ ¬ 𝐿 ∈ ℕ0 ) )
16 nn0re ⊢ ( 𝐿 ∈ ℕ0 → 𝐿 ∈ ℝ )
17 nn0re ⊢ ( 𝐹 ∈ ℕ0 → 𝐹 ∈ ℝ )
18 ltnle ⊢ ( ( 𝐿 ∈ ℝ ∧ 𝐹 ∈ ℝ ) → ( 𝐿 < 𝐹 ↔ ¬ 𝐹 ≤ 𝐿 ) )
19 16 17 18 syl2anr ⊢ ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝐿 < 𝐹 ↔ ¬ 𝐹 ≤ 𝐿 ) )
20 nn0z ⊢ ( 𝐹 ∈ ℕ0 → 𝐹 ∈ ℤ )
21 nn0z ⊢ ( 𝐿 ∈ ℕ0 → 𝐿 ∈ ℤ )
22 20 21 anim12i ⊢ ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) )
23 22 anim2i ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) )
24 3anass ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ↔ ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) )
25 23 24 sylibr ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) )
26 25 adantr ⊢ ( ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝐿 < 𝐹 ) → ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) )
27 17 16 anim12ci ⊢ ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝐿 ∈ ℝ ∧ 𝐹 ∈ ℝ ) )
28 27 adantl ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝐿 ∈ ℝ ∧ 𝐹 ∈ ℝ ) )
29 ltle ⊢ ( ( 𝐿 ∈ ℝ ∧ 𝐹 ∈ ℝ ) → ( 𝐿 < 𝐹 → 𝐿 ≤ 𝐹 ) )
30 28 29 syl ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝐿 < 𝐹 → 𝐿 ≤ 𝐹 ) )
31 30 imp ⊢ ( ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝐿 < 𝐹 ) → 𝐿 ≤ 𝐹 )
32 31 3mix2d ⊢ ( ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝐿 < 𝐹 ) → ( 𝐹 < 0 ∨ 𝐿 ≤ 𝐹 ∨ ( ♯ ‘ 𝑆 ) < 𝐿 ) )
33 swrdnd ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ( 𝐹 < 0 ∨ 𝐿 ≤ 𝐹 ∨ ( ♯ ‘ 𝑆 ) < 𝐿 ) → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) )
34 26 32 33 sylc ⊢ ( ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝐿 < 𝐹 ) → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ )
35 34 ex ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝐿 < 𝐹 → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) )
36 35 expcom ⊢ ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑆 ∈ Word 𝑉 → ( 𝐿 < 𝐹 → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) ) )
37 36 com23 ⊢ ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝐿 < 𝐹 → ( 𝑆 ∈ Word 𝑉 → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) ) )
38 19 37 sylbird ⊢ ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( ¬ 𝐹 ≤ 𝐿 → ( 𝑆 ∈ Word 𝑉 → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) ) )
39 15 38 sylbir ⊢ ( ¬ ( ¬ 𝐹 ∈ ℕ0 ∨ ¬ 𝐿 ∈ ℕ0 ) → ( ¬ 𝐹 ≤ 𝐿 → ( 𝑆 ∈ Word 𝑉 → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) ) )
40 39 imp ⊢ ( ( ¬ ( ¬ 𝐹 ∈ ℕ0 ∨ ¬ 𝐿 ∈ ℕ0 ) ∧ ¬ 𝐹 ≤ 𝐿 ) → ( 𝑆 ∈ Word 𝑉 → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) )
41 14 40 jaoi3 ⊢ ( ( ( ¬ 𝐹 ∈ ℕ0 ∨ ¬ 𝐿 ∈ ℕ0 ) ∨ ¬ 𝐹 ≤ 𝐿 ) → ( 𝑆 ∈ Word 𝑉 → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) )
42 10 41 sylbi ⊢ ( ( ¬ 𝐹 ∈ ℕ0 ∨ ¬ 𝐿 ∈ ℕ0 ∨ ¬ 𝐹 ≤ 𝐿 ) → ( 𝑆 ∈ Word 𝑉 → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) )
43 3anor ⊢ ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝐹 ≤ 𝐿 ) ↔ ¬ ( ¬ 𝐹 ∈ ℕ0 ∨ ¬ 𝐿 ∈ ℕ0 ∨ ¬ 𝐹 ≤ 𝐿 ) )
44 pm2.24 ⊢ ( 𝐿 ∈ ℕ0 → ( ¬ 𝐿 ∈ ℕ0 → ( 𝑆 ∈ Word 𝑉 → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) ) )
45 44 3ad2ant2 ⊢ ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝐹 ≤ 𝐿 ) → ( ¬ 𝐿 ∈ ℕ0 → ( 𝑆 ∈ Word 𝑉 → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) ) )
46 45 com12 ⊢ ( ¬ 𝐿 ∈ ℕ0 → ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝐹 ≤ 𝐿 ) → ( 𝑆 ∈ Word 𝑉 → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) ) )
47 pm2.24 ⊢ ( ( ♯ ‘ 𝑆 ) ∈ ℕ0 → ( ¬ ( ♯ ‘ 𝑆 ) ∈ ℕ0 → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) )
48 lencl ⊢ ( 𝑆 ∈ Word 𝑉 → ( ♯ ‘ 𝑆 ) ∈ ℕ0 )
49 47 48 syl11 ⊢ ( ¬ ( ♯ ‘ 𝑆 ) ∈ ℕ0 → ( 𝑆 ∈ Word 𝑉 → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) )
50 49 a1d ⊢ ( ¬ ( ♯ ‘ 𝑆 ) ∈ ℕ0 → ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝐹 ≤ 𝐿 ) → ( 𝑆 ∈ Word 𝑉 → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) ) )
51 48 nn0red ⊢ ( 𝑆 ∈ Word 𝑉 → ( ♯ ‘ 𝑆 ) ∈ ℝ )
52 16 3ad2ant2 ⊢ ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝐹 ≤ 𝐿 ) → 𝐿 ∈ ℝ )
53 ltnle ⊢ ( ( ( ♯ ‘ 𝑆 ) ∈ ℝ ∧ 𝐿 ∈ ℝ ) → ( ( ♯ ‘ 𝑆 ) < 𝐿 ↔ ¬ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) )
54 51 52 53 syl2anr ⊢ ( ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝐹 ≤ 𝐿 ) ∧ 𝑆 ∈ Word 𝑉 ) → ( ( ♯ ‘ 𝑆 ) < 𝐿 ↔ ¬ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) )
55 simpr ⊢ ( ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝐹 ≤ 𝐿 ) ∧ 𝑆 ∈ Word 𝑉 ) → 𝑆 ∈ Word 𝑉 )
56 20 3ad2ant1 ⊢ ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝐹 ≤ 𝐿 ) → 𝐹 ∈ ℤ )
57 56 adantr ⊢ ( ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝐹 ≤ 𝐿 ) ∧ 𝑆 ∈ Word 𝑉 ) → 𝐹 ∈ ℤ )
58 21 3ad2ant2 ⊢ ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝐹 ≤ 𝐿 ) → 𝐿 ∈ ℤ )
59 58 adantr ⊢ ( ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝐹 ≤ 𝐿 ) ∧ 𝑆 ∈ Word 𝑉 ) → 𝐿 ∈ ℤ )
60 55 57 59 3jca ⊢ ( ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝐹 ≤ 𝐿 ) ∧ 𝑆 ∈ Word 𝑉 ) → ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) )
61 3mix3 ⊢ ( ( ♯ ‘ 𝑆 ) < 𝐿 → ( 𝐹 < 0 ∨ 𝐿 ≤ 𝐹 ∨ ( ♯ ‘ 𝑆 ) < 𝐿 ) )
62 60 61 33 syl2im ⊢ ( ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝐹 ≤ 𝐿 ) ∧ 𝑆 ∈ Word 𝑉 ) → ( ( ♯ ‘ 𝑆 ) < 𝐿 → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) )
63 54 62 sylbird ⊢ ( ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝐹 ≤ 𝐿 ) ∧ 𝑆 ∈ Word 𝑉 ) → ( ¬ 𝐿 ≤ ( ♯ ‘ 𝑆 ) → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) )
64 63 com12 ⊢ ( ¬ 𝐿 ≤ ( ♯ ‘ 𝑆 ) → ( ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝐹 ≤ 𝐿 ) ∧ 𝑆 ∈ Word 𝑉 ) → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) )
65 64 expd ⊢ ( ¬ 𝐿 ≤ ( ♯ ‘ 𝑆 ) → ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝐹 ≤ 𝐿 ) → ( 𝑆 ∈ Word 𝑉 → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) ) )
66 46 50 65 3jaoi ⊢ ( ( ¬ 𝐿 ∈ ℕ0 ∨ ¬ ( ♯ ‘ 𝑆 ) ∈ ℕ0 ∨ ¬ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) → ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝐹 ≤ 𝐿 ) → ( 𝑆 ∈ Word 𝑉 → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) ) )
67 43 66 biimtrrid ⊢ ( ( ¬ 𝐿 ∈ ℕ0 ∨ ¬ ( ♯ ‘ 𝑆 ) ∈ ℕ0 ∨ ¬ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) → ( ¬ ( ¬ 𝐹 ∈ ℕ0 ∨ ¬ 𝐿 ∈ ℕ0 ∨ ¬ 𝐹 ≤ 𝐿 ) → ( 𝑆 ∈ Word 𝑉 → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) ) )
68 67 impcom ⊢ ( ( ¬ ( ¬ 𝐹 ∈ ℕ0 ∨ ¬ 𝐿 ∈ ℕ0 ∨ ¬ 𝐹 ≤ 𝐿 ) ∧ ( ¬ 𝐿 ∈ ℕ0 ∨ ¬ ( ♯ ‘ 𝑆 ) ∈ ℕ0 ∨ ¬ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 ∈ Word 𝑉 → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) )
69 42 68 jaoi3 ⊢ ( ( ( ¬ 𝐹 ∈ ℕ0 ∨ ¬ 𝐿 ∈ ℕ0 ∨ ¬ 𝐹 ≤ 𝐿 ) ∨ ( ¬ 𝐿 ∈ ℕ0 ∨ ¬ ( ♯ ‘ 𝑆 ) ∈ ℕ0 ∨ ¬ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 ∈ Word 𝑉 → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) )
70 69 com12 ⊢ ( 𝑆 ∈ Word 𝑉 → ( ( ( ¬ 𝐹 ∈ ℕ0 ∨ ¬ 𝐿 ∈ ℕ0 ∨ ¬ 𝐹 ≤ 𝐿 ) ∨ ( ¬ 𝐿 ∈ ℕ0 ∨ ¬ ( ♯ ‘ 𝑆 ) ∈ ℕ0 ∨ ¬ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) )
71 9 70 biimtrid ⊢ ( 𝑆 ∈ Word 𝑉 → ( ¬ ( 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) )