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

Metamath Proof Explorer

Theorem wrdnval

Description: Words of a fixed length are mappings from a fixed half-open integer interval. (Contributed by Alexander van der Vekens, 25-Mar-2018) (Proof shortened by AV, 13-May-2020)

Ref Expression
Assertion wrdnval 
|- ( ( V e. X /\ N e. NN0 ) -> { w e. Word V | ( # ` w ) = N } = ( V ^m ( 0 ..^ N ) ) )

Proof

Step Hyp Ref Expression
1 df-rab 
 |-  { w e. Word V | ( # ` w ) = N } = { w | ( w e. Word V /\ ( # ` w ) = N ) }
2 ovexd 
 |-  ( ( V e. X /\ N e. NN0 ) -> ( 0 ..^ N ) e. _V )
3 elmapg 
 |-  ( ( V e. X /\ ( 0 ..^ N ) e. _V ) -> ( w e. ( V ^m ( 0 ..^ N ) ) <-> w : ( 0 ..^ N ) --> V ) )
4 2 3 syldan 
 |-  ( ( V e. X /\ N e. NN0 ) -> ( w e. ( V ^m ( 0 ..^ N ) ) <-> w : ( 0 ..^ N ) --> V ) )
5 iswrdi 
 |-  ( w : ( 0 ..^ N ) --> V -> w e. Word V )
6 5 adantl 
 |-  ( ( ( V e. X /\ N e. NN0 ) /\ w : ( 0 ..^ N ) --> V ) -> w e. Word V )
7 fnfzo0hash 
 |-  ( ( N e. NN0 /\ w : ( 0 ..^ N ) --> V ) -> ( # ` w ) = N )
8 7 adantll 
 |-  ( ( ( V e. X /\ N e. NN0 ) /\ w : ( 0 ..^ N ) --> V ) -> ( # ` w ) = N )
9 6 8 jca 
 |-  ( ( ( V e. X /\ N e. NN0 ) /\ w : ( 0 ..^ N ) --> V ) -> ( w e. Word V /\ ( # ` w ) = N ) )
10 9 ex 
 |-  ( ( V e. X /\ N e. NN0 ) -> ( w : ( 0 ..^ N ) --> V -> ( w e. Word V /\ ( # ` w ) = N ) ) )
11 wrdf 
 |-  ( w e. Word V -> w : ( 0 ..^ ( # ` w ) ) --> V )
12 oveq2 
 |-  ( ( # ` w ) = N -> ( 0 ..^ ( # ` w ) ) = ( 0 ..^ N ) )
13 12 feq2d 
 |-  ( ( # ` w ) = N -> ( w : ( 0 ..^ ( # ` w ) ) --> V <-> w : ( 0 ..^ N ) --> V ) )
14 11 13 syl5ibcom 
 |-  ( w e. Word V -> ( ( # ` w ) = N -> w : ( 0 ..^ N ) --> V ) )
15 14 imp 
 |-  ( ( w e. Word V /\ ( # ` w ) = N ) -> w : ( 0 ..^ N ) --> V )
16 10 15 impbid1 
 |-  ( ( V e. X /\ N e. NN0 ) -> ( w : ( 0 ..^ N ) --> V <-> ( w e. Word V /\ ( # ` w ) = N ) ) )
17 4 16 bitrd 
 |-  ( ( V e. X /\ N e. NN0 ) -> ( w e. ( V ^m ( 0 ..^ N ) ) <-> ( w e. Word V /\ ( # ` w ) = N ) ) )
18 17 eqabdv 
 |-  ( ( V e. X /\ N e. NN0 ) -> ( V ^m ( 0 ..^ N ) ) = { w | ( w e. Word V /\ ( # ` w ) = N ) } )
19 1 18 eqtr4id 
 |-  ( ( V e. X /\ N e. NN0 ) -> { w e. Word V | ( # ` w ) = N } = ( V ^m ( 0 ..^ N ) ) )