Metamath Proof Explorer

Theorem swrdnd2

Description: Value of the subword extractor outside its intended domain. (Contributed by Alexander van der Vekens, 24-May-2018)

Ref Expression
Assertion swrdnd2 ⊢W∈WordV∧A∈ℤ∧B∈ℤ→B≤A∨W≤A∨B≤0→WsubstrAB=∅

Proof

Step Hyp Ref Expression
1 3orass ⊢B≤A∨W≤A∨B≤0↔B≤A∨W≤A∨B≤0
2 pm2.24 ⊢B≤A→¬B≤A→W∈WordV∧A∈ℤ∧B∈ℤ→WsubstrAB=∅
3 swrdval ⊢W∈WordV∧A∈ℤ∧B∈ℤ→WsubstrAB=ifA..^B⊆dom⁡Wx∈0..^B−A⟼W⁡x+A∅
4 3 ad2antrr ⊢W∈WordV∧A∈ℤ∧B∈ℤ∧W≤A∨B≤0∧¬B≤A→WsubstrAB=ifA..^B⊆dom⁡Wx∈0..^B−A⟼W⁡x+A∅
5 wrddm ⊢W∈WordV→dom⁡W=0..^W
6 lencl ⊢W∈WordV→W∈ℕ0
7 3anass ⊢W∈ℕ0∧A∈ℤ∧B∈ℤ↔W∈ℕ0∧A∈ℤ∧B∈ℤ
8 ssfzoulel ⊢W∈ℕ0∧A∈ℤ∧B∈ℤ→W≤A∨B≤0→A..^B⊆0..^W→B≤A
9 8 imp ⊢W∈ℕ0∧A∈ℤ∧B∈ℤ∧W≤A∨B≤0→A..^B⊆0..^W→B≤A
10 7 9 sylanbr ⊢W∈ℕ0∧A∈ℤ∧B∈ℤ∧W≤A∨B≤0→A..^B⊆0..^W→B≤A
11 10 con3dimp ⊢W∈ℕ0∧A∈ℤ∧B∈ℤ∧W≤A∨B≤0∧¬B≤A→¬A..^B⊆0..^W
12 sseq2 ⊢dom⁡W=0..^W→A..^B⊆dom⁡W↔A..^B⊆0..^W
13 12 notbid ⊢dom⁡W=0..^W→¬A..^B⊆dom⁡W↔¬A..^B⊆0..^W
14 11 13 imbitrrid ⊢dom⁡W=0..^W→W∈ℕ0∧A∈ℤ∧B∈ℤ∧W≤A∨B≤0∧¬B≤A→¬A..^B⊆dom⁡W
15 14 exp5j ⊢dom⁡W=0..^W→W∈ℕ0→A∈ℤ∧B∈ℤ→W≤A∨B≤0→¬B≤A→¬A..^B⊆dom⁡W
16 5 6 15 sylc ⊢W∈WordV→A∈ℤ∧B∈ℤ→W≤A∨B≤0→¬B≤A→¬A..^B⊆dom⁡W
17 16 3impib ⊢W∈WordV∧A∈ℤ∧B∈ℤ→W≤A∨B≤0→¬B≤A→¬A..^B⊆dom⁡W
18 17 imp31 ⊢W∈WordV∧A∈ℤ∧B∈ℤ∧W≤A∨B≤0∧¬B≤A→¬A..^B⊆dom⁡W
19 18 iffalsed ⊢W∈WordV∧A∈ℤ∧B∈ℤ∧W≤A∨B≤0∧¬B≤A→ifA..^B⊆dom⁡Wx∈0..^B−A⟼W⁡x+A∅=∅
20 4 19 eqtrd ⊢W∈WordV∧A∈ℤ∧B∈ℤ∧W≤A∨B≤0∧¬B≤A→WsubstrAB=∅
21 20 ex ⊢W∈WordV∧A∈ℤ∧B∈ℤ∧W≤A∨B≤0→¬B≤A→WsubstrAB=∅
22 21 expcom ⊢W≤A∨B≤0→W∈WordV∧A∈ℤ∧B∈ℤ→¬B≤A→WsubstrAB=∅
23 22 com23 ⊢W≤A∨B≤0→¬B≤A→W∈WordV∧A∈ℤ∧B∈ℤ→WsubstrAB=∅
24 2 23 jaoi ⊢B≤A∨W≤A∨B≤0→¬B≤A→W∈WordV∧A∈ℤ∧B∈ℤ→WsubstrAB=∅
25 swrdlend ⊢W∈WordV∧A∈ℤ∧B∈ℤ→B≤A→WsubstrAB=∅
26 25 com12 ⊢B≤A→W∈WordV∧A∈ℤ∧B∈ℤ→WsubstrAB=∅
27 24 26 pm2.61d2 ⊢B≤A∨W≤A∨B≤0→W∈WordV∧A∈ℤ∧B∈ℤ→WsubstrAB=∅
28 1 27 sylbi ⊢B≤A∨W≤A∨B≤0→W∈WordV∧A∈ℤ∧B∈ℤ→WsubstrAB=∅
29 28 com12 ⊢W∈WordV∧A∈ℤ∧B∈ℤ→B≤A∨W≤A∨B≤0→WsubstrAB=∅