Theorem wrdmap

Description: Words as a mapping. (Contributed by Thierry Arnoux, 4-Mar-2020)

	Ref	Expression
Assertion	wrdmap	|- ( ( V e. X /\ N e. NN0 ) -> ( ( W e. Word V /\ ( # ` W ) = N ) <-> W e. ( V ^m ( 0 ..^ N ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fveqeq2	|- ( w = W -> ( ( # ` w ) = N <-> ( # ` W ) = N ) )
2	1	elrab	|- ( W e. { w e. Word V | ( # ` w ) = N } <-> ( W e. Word V /\ ( # ` W ) = N ) )
3		wrdnval	|- ( ( V e. X /\ N e. NN0 ) -> { w e. Word V | ( # ` w ) = N } = ( V ^m ( 0 ..^ N ) ) )
4	3	eleq2d	|- ( ( V e. X /\ N e. NN0 ) -> ( W e. { w e. Word V | ( # ` w ) = N } <-> W e. ( V ^m ( 0 ..^ N ) ) ) )
5	2 4	bitr3id	|- ( ( V e. X /\ N e. NN0 ) -> ( ( W e. Word V /\ ( # ` W ) = N ) <-> W e. ( V ^m ( 0 ..^ N ) ) ) )