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 ⊢ W ∈ Word V ∧ L ∉ 0 … W → W prefix L = ∅

Proof

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