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

Metamath Proof Explorer

Theorem wrddm

Description: The indices of a word (i.e. its domain regarded as function) are elements of an open range of nonnegative integers (of length equal to the length of the word). (Contributed by AV, 2-May-2020)

		Ref	Expression
	Assertion	wrddm	⊢ ( 𝑊 ∈ Word 𝑆 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )

Proof

Step	Hyp	Ref	Expression
1		wrdf	⊢ ( 𝑊 ∈ Word 𝑆 → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑆 )
2	1	fdmd	⊢ ( 𝑊 ∈ Word 𝑆 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )