Metamath Proof Explorer


Theorem wrdexb

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 SVWordSV

Proof

Step Hyp Ref Expression
1 wrdexg SVWordSV
2 opex 0sV
3 2 snid 0s0s
4 snopiswrd sS0sWordS
5 elunii 0s0s0sWordS0sWordS
6 3 4 5 sylancr sS0sWordS
7 c0ex 0V
8 vex sV
9 7 8 opeluu 0sWordS0WordSsWordS
10 6 9 syl sS0WordSsWordS
11 10 simprd sSsWordS
12 11 ssriv SWordS
13 uniexg WordSVWordSV
14 uniexg WordSVWordSV
15 uniexg WordSVWordSV
16 13 14 15 3syl WordSVWordSV
17 ssexg SWordSWordSVSV
18 12 16 17 sylancr WordSVSV
19 1 18 impbii SVWordSV