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 
|- ( S e. _V <-> Word S e. _V )

Proof

Step Hyp Ref Expression
1 wrdexg 
 |-  ( S e. _V -> Word S e. _V )
2 opex 
 |-  <. 0 , s >. e. _V
3 2 snid 
 |-  <. 0 , s >. e. { <. 0 , s >. }
4 snopiswrd 
 |-  ( s e. S -> { <. 0 , s >. } e. Word S )
5 elunii 
 |-  ( ( <. 0 , s >. e. { <. 0 , s >. } /\ { <. 0 , s >. } e. Word S ) -> <. 0 , s >. e. U. Word S )
6 3 4 5 sylancr 
 |-  ( s e. S -> <. 0 , s >. e. U. Word S )
7 c0ex 
 |-  0 e. _V
8 vex 
 |-  s e. _V
9 7 8 opeluu 
 |-  ( <. 0 , s >. e. U. Word S -> ( 0 e. U. U. U. Word S /\ s e. U. U. U. Word S ) )
10 6 9 syl 
 |-  ( s e. S -> ( 0 e. U. U. U. Word S /\ s e. U. U. U. Word S ) )
11 10 simprd 
 |-  ( s e. S -> s e. U. U. U. Word S )
12 11 ssriv 
 |-  S C_ U. U. U. Word S
13 uniexg 
 |-  ( Word S e. _V -> U. Word S e. _V )
14 uniexg 
 |-  ( U. Word S e. _V -> U. U. Word S e. _V )
15 uniexg 
 |-  ( U. U. Word S e. _V -> U. U. U. Word S e. _V )
16 13 14 15 3syl 
 |-  ( Word S e. _V -> U. U. U. Word S e. _V )
17 ssexg 
 |-  ( ( S C_ U. U. U. Word S /\ U. U. U. Word S e. _V ) -> S e. _V )
18 12 16 17 sylancr 
 |-  ( Word S e. _V -> S e. _V )
19 1 18 impbii 
 |-  ( S e. _V <-> Word S e. _V )