Description: Value of the subword extractor in its intended domain. (Contributed by Stefan O'Rear, 15-Aug-2015) (Proof shortened by AV, 2-May-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | swrdval2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1 | |
|
2 | elfzelz | |
|
3 | 2 | 3ad2ant2 | |
4 | elfzelz | |
|
5 | 4 | 3ad2ant3 | |
6 | swrdval | |
|
7 | 1 3 5 6 | syl3anc | |
8 | elfzuz | |
|
9 | 8 | 3ad2ant2 | |
10 | fzoss1 | |
|
11 | 9 10 | syl | |
12 | elfzuz3 | |
|
13 | 12 | 3ad2ant3 | |
14 | fzoss2 | |
|
15 | 13 14 | syl | |
16 | 11 15 | sstrd | |
17 | wrddm | |
|
18 | 17 | 3ad2ant1 | |
19 | 16 18 | sseqtrrd | |
20 | 19 | iftrued | |
21 | 7 20 | eqtrd | |