This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iswrd

Description: Property of being a word over a set with an existential quantifier over the length. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by Mario Carneiro, 26-Feb-2016) (Proof shortened by AV, 13-May-2020)

Ref Expression
Assertion iswrd 
|- ( W e. Word S <-> E. l e. NN0 W : ( 0 ..^ l ) --> S )

Proof

Step Hyp Ref Expression
1 df-word 
 |-  Word S = { w | E. l e. NN0 w : ( 0 ..^ l ) --> S }
2 1 eleq2i 
 |-  ( W e. Word S <-> W e. { w | E. l e. NN0 w : ( 0 ..^ l ) --> S } )
3 ovex 
 |-  ( 0 ..^ l ) e. _V
4 fex 
 |-  ( ( W : ( 0 ..^ l ) --> S /\ ( 0 ..^ l ) e. _V ) -> W e. _V )
5 3 4 mpan2 
 |-  ( W : ( 0 ..^ l ) --> S -> W e. _V )
6 5 rexlimivw 
 |-  ( E. l e. NN0 W : ( 0 ..^ l ) --> S -> W e. _V )
7 feq1 
 |-  ( w = W -> ( w : ( 0 ..^ l ) --> S <-> W : ( 0 ..^ l ) --> S ) )
8 7 rexbidv 
 |-  ( w = W -> ( E. l e. NN0 w : ( 0 ..^ l ) --> S <-> E. l e. NN0 W : ( 0 ..^ l ) --> S ) )
9 6 8 elab3 
 |-  ( W e. { w | E. l e. NN0 w : ( 0 ..^ l ) --> S } <-> E. l e. NN0 W : ( 0 ..^ l ) --> S )
10 2 9 bitri 
 |-  ( W e. Word S <-> E. l e. NN0 W : ( 0 ..^ l ) --> S )