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