wrdffz

Description: A word is a function from a finite interval of integers. (Contributed by AV, 10-Feb-2021)

		Ref	Expression
	Assertion	wrdffz	$⊢ W \in Word S \to W : (0 \dots \|W\| - 1) ⟶ S$

Step	Hyp	Ref	Expression
1		wrdf	$⊢ W \in Word S \to W : (0 ..^\|W\|) ⟶ S$
2		lencl	$⊢ W \in Word S \to \|W\| \in ℕ_{0}$
3	2	nn0zd	$⊢ W \in Word S \to \|W\| \in ℤ$
4		fzoval	$⊢ \|W\| \in ℤ \to (0 ..^\|W\|) = (0 \dots \|W\| - 1)$
5	3 4	syl	$⊢ W \in Word S \to (0 ..^\|W\|) = (0 \dots \|W\| - 1)$
6	5	feq2d	$⊢ W \in Word S \to (W : (0 ..^\|W\|) ⟶ S \leftrightarrow W : (0 \dots \|W\| - 1) ⟶ S)$
7	1 6	mpbid	$⊢ W \in Word S \to W : (0 \dots \|W\| - 1) ⟶ S$

Metamath Proof Explorer