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∈WordV∧L∉0…W→WprefixL=∅

Proof

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