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 )