Metamath Proof Explorer

Theorem wrdexg

Description: The set of words over a set is a set. (Contributed by Mario Carneiro, 26-Feb-2016) (Proof shortened by JJ, 18-Nov-2022)

Ref Expression
Assertion wrdexg 
|- ( S e. V -> Word S e. _V )

Proof

Step Hyp Ref Expression
1 wrdval 
 |-  ( S e. V -> Word S = U_ l e. NN0 ( S ^m ( 0 ..^ l ) ) )
2 nn0ex 
 |-  NN0 e. _V
3 ovexd 
 |-  ( ( S e. V /\ l e. NN0 ) -> ( S ^m ( 0 ..^ l ) ) e. _V )
4 3 ralrimiva 
 |-  ( S e. V -> A. l e. NN0 ( S ^m ( 0 ..^ l ) ) e. _V )
5 iunexg 
 |-  ( ( NN0 e. _V /\ A. l e. NN0 ( S ^m ( 0 ..^ l ) ) e. _V ) -> U_ l e. NN0 ( S ^m ( 0 ..^ l ) ) e. _V )
6 2 4 5 sylancr 
 |-  ( S e. V -> U_ l e. NN0 ( S ^m ( 0 ..^ l ) ) e. _V )
7 1 6 eqeltrd 
 |-  ( S e. V -> Word S e. _V )