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 pfxnndmnd ⊢ ¬ W ∈ V ∧ L ∈ ℕ 0 → W prefix L = ∅
16 14 15 nsyl5 ⊢ ¬ L ∈ ℕ 0 → W prefix L = ∅
17 16 a1d ⊢ ¬ L ∈ ℕ 0 → W ∈ Word V → W prefix L = ∅
18 notnotb ⊢ L ∈ ℕ 0 ↔ ¬ ¬ L ∈ ℕ 0
19 11 nn0red ⊢ W ∈ Word V → W ∈ ℝ
20 nn0re ⊢ L ∈ ℕ 0 → L ∈ ℝ
21 ltnle ⊢ W ∈ ℝ ∧ L ∈ ℝ → W < L ↔ ¬ L ≤ W
22 19 20 21 syl2an ⊢ W ∈ Word V ∧ L ∈ ℕ 0 → W < L ↔ ¬ L ≤ W
23 pfxnd ⊢ W ∈ Word V ∧ L ∈ ℕ 0 ∧ W < L → W prefix L = ∅
24 23 3expia ⊢ W ∈ Word V ∧ L ∈ ℕ 0 → W < L → W prefix L = ∅
25 22 24 sylbird ⊢ W ∈ Word V ∧ L ∈ ℕ 0 → ¬ L ≤ W → W prefix L = ∅
26 25 expcom ⊢ L ∈ ℕ 0 → W ∈ Word V → ¬ L ≤ W → W prefix L = ∅
27 26 com23 ⊢ L ∈ ℕ 0 → ¬ L ≤ W → W ∈ Word V → W prefix L = ∅
28 18 27 sylbir ⊢ ¬ ¬ L ∈ ℕ 0 → ¬ L ≤ W → W ∈ Word V → W prefix L = ∅
29 28 imp ⊢ ¬ ¬ L ∈ ℕ 0 ∧ ¬ L ≤ W → W ∈ Word V → W prefix L = ∅
30 17 29 jaoi3 ⊢ ¬ L ∈ ℕ 0 ∨ ¬ L ≤ W → W ∈ Word V → W prefix L = ∅
31 30 orcoms ⊢ ¬ L ≤ W ∨ ¬ L ∈ ℕ 0 → W ∈ Word V → W prefix L = ∅
32 13 31 jaoi ⊢ ¬ W ∈ ℕ 0 ∨ ¬ L ≤ W ∨ ¬ L ∈ ℕ 0 → W ∈ Word V → W prefix L = ∅
33 10 32 sylbi ⊢ ¬ W ∈ ℕ 0 ∨ ¬ L ≤ W ∨ ¬ L ∈ ℕ 0 → W ∈ Word V → W prefix L = ∅
34 9 33 sylbi ⊢ ¬ L ∈ ℕ 0 ∨ ¬ W ∈ ℕ 0 ∨ ¬ L ≤ W → W ∈ Word V → W prefix L = ∅
35 34 com12 ⊢ W ∈ Word V → ¬ L ∈ ℕ 0 ∨ ¬ W ∈ ℕ 0 ∨ ¬ L ≤ W → W prefix L = ∅
36 8 35 sylbid ⊢ W ∈ Word V → L ∉ 0 … W → W prefix L = ∅
37 36 imp ⊢ W ∈ Word V ∧ L ∉ 0 … W → W prefix L = ∅