wrdf

Description: A word is a zero-based sequence with a recoverable upper limit. (Contributed by Stefan O'Rear, 15-Aug-2015)

		Ref	Expression
	Assertion	wrdf	$⊢ W \in Word S \to W : (0 ..^\|W\|) ⟶ S$

Step	Hyp	Ref	Expression
1		iswrd	$⊢ W \in Word S \leftrightarrow \exists l \in ℕ_{0} W : (0 ..^l) ⟶ S$
2		simpr	$⊢ (l \in ℕ_{0} \land W : (0 ..^l) ⟶ S) \to W : (0 ..^l) ⟶ S$
3		fnfzo0hash	$⊢ (l \in ℕ_{0} \land W : (0 ..^l) ⟶ S) \to \|W\| = l$
4	3	oveq2d	$⊢ (l \in ℕ_{0} \land W : (0 ..^l) ⟶ S) \to (0 ..^\|W\|) = (0 ..^l)$
5	4	feq2d	$⊢ (l \in ℕ_{0} \land W : (0 ..^l) ⟶ S) \to (W : (0 ..^\|W\|) ⟶ S \leftrightarrow W : (0 ..^l) ⟶ S)$
6	2 5	mpbird	$⊢ (l \in ℕ_{0} \land W : (0 ..^l) ⟶ S) \to W : (0 ..^\|W\|) ⟶ S$
7	6	rexlimiva	$⊢ \exists l \in ℕ_{0} W : (0 ..^l) ⟶ S \to W : (0 ..^\|W\|) ⟶ S$
8	1 7	sylbi	$⊢ W \in Word S \to W : (0 ..^\|W\|) ⟶ S$

Metamath Proof Explorer