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

Metamath Proof Explorer

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 ) ) ) )