Theorem wrdfd

Description: A word is a zero-based sequence with a recoverable upper limit, deduction version. (Contributed by Thierry Arnoux, 22-Dec-2021)

	Ref	Expression
Hypotheses	wrdfd.n	$$⊢\phi \to N=\left|W\right|$$
	wrdfd.w	$$⊢\phi \to W\in \mathrm{Word}S$$
Assertion	wrdfd	$$⊢\phi \to W:\left(0..^N\right)⟶S$$

Proof

Step	Hyp	Ref	Expression
1		wrdfd.n	$$⊢\phi \to N=\left|W\right|$$
2		wrdfd.w	$$⊢\phi \to W\in \mathrm{Word}S$$
3		wrdf	$$⊢W\in \mathrm{Word}S\to W:\left(0..^\left|W\right|\right)⟶S$$
4	2 3	syl	$$⊢\phi \to W:\left(0..^\left|W\right|\right)⟶S$$
5	1	oveq2d	$$⊢\phi \to \left(0..^N\right)=\left(0..^\left|W\right|\right)$$
6	5	feq2d	$$⊢\phi \to \left(W:\left(0..^N\right)⟶S\leftrightarrow W:\left(0..^\left|W\right|\right)⟶S\right)$$
7	4 6	mpbird	$$⊢\phi \to W:\left(0..^N\right)⟶S$$