Metamath Proof Explorer

Theorem pfxnd0

Description: The value of a prefix operation for a length argument not in the range of the word length is the empty set. (This is due to our definition of function values for out-of-domain arguments, see ndmfv ). (Contributed by AV, 3-Dec-2022)

Ref Expression
Assertion pfxnd0 ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∉ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 prefix 𝐿 ) = ∅ )

Proof

Step Hyp Ref Expression
1 df-nel ⊢ ( 𝐿 ∉ ( 0 ... ( ♯ ‘ 𝑊 ) ) ↔ ¬ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
2 1 a1i ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝐿 ∉ ( 0 ... ( ♯ ‘ 𝑊 ) ) ↔ ¬ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) )
3 elfz2nn0 ⊢ ( 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ↔ ( 𝐿 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) )
4 3 a1i ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ↔ ( 𝐿 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) ) )
5 4 notbid ⊢ ( 𝑊 ∈ Word 𝑉 → ( ¬ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ↔ ¬ ( 𝐿 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) ) )
6 3ianor ⊢ ( ¬ ( 𝐿 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) ↔ ( ¬ 𝐿 ∈ ℕ0 ∨ ¬ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∨ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) )
7 6 a1i ⊢ ( 𝑊 ∈ Word 𝑉 → ( ¬ ( 𝐿 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) ↔ ( ¬ 𝐿 ∈ ℕ0 ∨ ¬ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∨ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) ) )
8 2 5 7 3bitrd ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝐿 ∉ ( 0 ... ( ♯ ‘ 𝑊 ) ) ↔ ( ¬ 𝐿 ∈ ℕ0 ∨ ¬ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∨ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) ) )
9 3orrot ⊢ ( ( ¬ 𝐿 ∈ ℕ0 ∨ ¬ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∨ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) ↔ ( ¬ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∨ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ∨ ¬ 𝐿 ∈ ℕ0 ) )
10 3orass ⊢ ( ( ¬ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∨ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ∨ ¬ 𝐿 ∈ ℕ0 ) ↔ ( ¬ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∨ ( ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ∨ ¬ 𝐿 ∈ ℕ0 ) ) )
11 lencl ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
12 11 pm2.24d ⊢ ( 𝑊 ∈ Word 𝑉 → ( ¬ ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( 𝑊 prefix 𝐿 ) = ∅ ) )
13 12 com12 ⊢ ( ¬ ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( 𝑊 ∈ Word 𝑉 → ( 𝑊 prefix 𝐿 ) = ∅ ) )
14 simpr ⊢ ( ( 𝑊 ∈ V ∧ 𝐿 ∈ ℕ0 ) → 𝐿 ∈ ℕ0 )
15 pfxnndmnd ⊢ ( ¬ ( 𝑊 ∈ V ∧ 𝐿 ∈ ℕ0 ) → ( 𝑊 prefix 𝐿 ) = ∅ )
16 14 15 nsyl5 ⊢ ( ¬ 𝐿 ∈ ℕ0 → ( 𝑊 prefix 𝐿 ) = ∅ )
17 16 a1d ⊢ ( ¬ 𝐿 ∈ ℕ0 → ( 𝑊 ∈ Word 𝑉 → ( 𝑊 prefix 𝐿 ) = ∅ ) )
18 notnotb ⊢ ( 𝐿 ∈ ℕ0 ↔ ¬ ¬ 𝐿 ∈ ℕ0 )
19 11 nn0red ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℝ )
20 nn0re ⊢ ( 𝐿 ∈ ℕ0 → 𝐿 ∈ ℝ )
21 ltnle ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℝ ∧ 𝐿 ∈ ℝ ) → ( ( ♯ ‘ 𝑊 ) < 𝐿 ↔ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) )
22 19 20 21 syl2an ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℕ0 ) → ( ( ♯ ‘ 𝑊 ) < 𝐿 ↔ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) )
23 pfxnd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) < 𝐿 ) → ( 𝑊 prefix 𝐿 ) = ∅ )
24 23 3expia ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℕ0 ) → ( ( ♯ ‘ 𝑊 ) < 𝐿 → ( 𝑊 prefix 𝐿 ) = ∅ ) )
25 22 24 sylbird ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℕ0 ) → ( ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) → ( 𝑊 prefix 𝐿 ) = ∅ ) )
26 25 expcom ⊢ ( 𝐿 ∈ ℕ0 → ( 𝑊 ∈ Word 𝑉 → ( ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) → ( 𝑊 prefix 𝐿 ) = ∅ ) ) )
27 26 com23 ⊢ ( 𝐿 ∈ ℕ0 → ( ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) → ( 𝑊 ∈ Word 𝑉 → ( 𝑊 prefix 𝐿 ) = ∅ ) ) )
28 18 27 sylbir ⊢ ( ¬ ¬ 𝐿 ∈ ℕ0 → ( ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) → ( 𝑊 ∈ Word 𝑉 → ( 𝑊 prefix 𝐿 ) = ∅ ) ) )
29 28 imp ⊢ ( ( ¬ ¬ 𝐿 ∈ ℕ0 ∧ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑊 ∈ Word 𝑉 → ( 𝑊 prefix 𝐿 ) = ∅ ) )
30 17 29 jaoi3 ⊢ ( ( ¬ 𝐿 ∈ ℕ0 ∨ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑊 ∈ Word 𝑉 → ( 𝑊 prefix 𝐿 ) = ∅ ) )
31 30 orcoms ⊢ ( ( ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ∨ ¬ 𝐿 ∈ ℕ0 ) → ( 𝑊 ∈ Word 𝑉 → ( 𝑊 prefix 𝐿 ) = ∅ ) )
32 13 31 jaoi ⊢ ( ( ¬ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∨ ( ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ∨ ¬ 𝐿 ∈ ℕ0 ) ) → ( 𝑊 ∈ Word 𝑉 → ( 𝑊 prefix 𝐿 ) = ∅ ) )
33 10 32 sylbi ⊢ ( ( ¬ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∨ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ∨ ¬ 𝐿 ∈ ℕ0 ) → ( 𝑊 ∈ Word 𝑉 → ( 𝑊 prefix 𝐿 ) = ∅ ) )
34 9 33 sylbi ⊢ ( ( ¬ 𝐿 ∈ ℕ0 ∨ ¬ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∨ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑊 ∈ Word 𝑉 → ( 𝑊 prefix 𝐿 ) = ∅ ) )
35 34 com12 ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( ¬ 𝐿 ∈ ℕ0 ∨ ¬ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∨ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑊 prefix 𝐿 ) = ∅ ) )
36 8 35 sylbid ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝐿 ∉ ( 0 ... ( ♯ ‘ 𝑊 ) ) → ( 𝑊 prefix 𝐿 ) = ∅ ) )
37 36 imp ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∉ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 prefix 𝐿 ) = ∅ )