Description: The set of words over a set is a set, bidirectional version. (Contributed by Mario Carneiro, 26-Feb-2016) (Proof shortened by AV, 23-Nov-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | wrdexb | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wrdexg | |
|
2 | opex | |
|
3 | 2 | snid | |
4 | snopiswrd | |
|
5 | elunii | |
|
6 | 3 4 5 | sylancr | |
7 | c0ex | |
|
8 | vex | |
|
9 | 7 8 | opeluu | |
10 | 6 9 | syl | |
11 | 10 | simprd | |
12 | 11 | ssriv | |
13 | uniexg | |
|
14 | uniexg | |
|
15 | uniexg | |
|
16 | 13 14 15 | 3syl | |
17 | ssexg | |
|
18 | 12 16 17 | sylancr | |
19 | 1 18 | impbii | |