Step |
Hyp |
Ref |
Expression |
1 |
|
df-word |
|- Word S = { w | E. l e. NN0 w : ( 0 ..^ l ) --> S } |
2 |
|
eliun |
|- ( w e. U_ l e. NN0 ( S ^m ( 0 ..^ l ) ) <-> E. l e. NN0 w e. ( S ^m ( 0 ..^ l ) ) ) |
3 |
|
ovex |
|- ( 0 ..^ l ) e. _V |
4 |
|
elmapg |
|- ( ( S e. V /\ ( 0 ..^ l ) e. _V ) -> ( w e. ( S ^m ( 0 ..^ l ) ) <-> w : ( 0 ..^ l ) --> S ) ) |
5 |
3 4
|
mpan2 |
|- ( S e. V -> ( w e. ( S ^m ( 0 ..^ l ) ) <-> w : ( 0 ..^ l ) --> S ) ) |
6 |
5
|
rexbidv |
|- ( S e. V -> ( E. l e. NN0 w e. ( S ^m ( 0 ..^ l ) ) <-> E. l e. NN0 w : ( 0 ..^ l ) --> S ) ) |
7 |
2 6
|
syl5bb |
|- ( S e. V -> ( w e. U_ l e. NN0 ( S ^m ( 0 ..^ l ) ) <-> E. l e. NN0 w : ( 0 ..^ l ) --> S ) ) |
8 |
7
|
abbi2dv |
|- ( S e. V -> U_ l e. NN0 ( S ^m ( 0 ..^ l ) ) = { w | E. l e. NN0 w : ( 0 ..^ l ) --> S } ) |
9 |
1 8
|
eqtr4id |
|- ( S e. V -> Word S = U_ l e. NN0 ( S ^m ( 0 ..^ l ) ) ) |