Metamath Proof Explorer

Theorem wrdsymb0

Description: A symbol at a position "outside" of a word. (Contributed by Alexander van der Vekens, 26-May-2018) (Proof shortened by AV, 2-May-2020)

Ref Expression
Assertion wrdsymb0 ⊢W∈WordV∧I∈ℤ→I<0∨W≤I→W⁡I=∅

Proof

Step Hyp Ref Expression
1 wrddm ⊢W∈WordV→dom⁡W=0..^W
2 lencl ⊢W∈WordV→W∈ℕ0
3 2 nn0zd ⊢W∈WordV→W∈ℤ
4 simpr ⊢W∈ℤ∧I∈ℤ→I∈ℤ
5 0zd ⊢W∈ℤ∧I∈ℤ→0∈ℤ
6 simpl ⊢W∈ℤ∧I∈ℤ→W∈ℤ
7 nelfzo ⊢I∈ℤ∧0∈ℤ∧W∈ℤ→I∉0..^W↔I<0∨W≤I
8 4 5 6 7 syl3anc ⊢W∈ℤ∧I∈ℤ→I∉0..^W↔I<0∨W≤I
9 8 biimpar ⊢W∈ℤ∧I∈ℤ∧I<0∨W≤I→I∉0..^W
10 df-nel ⊢I∉0..^W↔¬I∈0..^W
11 9 10 sylib ⊢W∈ℤ∧I∈ℤ∧I<0∨W≤I→¬I∈0..^W
12 eleq2 ⊢dom⁡W=0..^W→I∈dom⁡W↔I∈0..^W
13 12 notbid ⊢dom⁡W=0..^W→¬I∈dom⁡W↔¬I∈0..^W
14 11 13 imbitrrid ⊢dom⁡W=0..^W→W∈ℤ∧I∈ℤ∧I<0∨W≤I→¬I∈dom⁡W
15 14 exp4c ⊢dom⁡W=0..^W→W∈ℤ→I∈ℤ→I<0∨W≤I→¬I∈dom⁡W
16 1 3 15 sylc ⊢W∈WordV→I∈ℤ→I<0∨W≤I→¬I∈dom⁡W
17 16 imp ⊢W∈WordV∧I∈ℤ→I<0∨W≤I→¬I∈dom⁡W
18 ndmfv ⊢¬I∈dom⁡W→W⁡I=∅
19 17 18 syl6 ⊢W∈WordV∧I∈ℤ→I<0∨W≤I→W⁡I=∅