wrdmap

Description: Words as a mapping. (Contributed by Thierry Arnoux, 4-Mar-2020)

		Ref	Expression
	Assertion	wrdmap	$⊢ (V \in X \land N \in ℕ_{0}) \to ((W \in Word V \land \|W\| = N) \leftrightarrow W \in (V^{(0 ..^N)}))$

Step	Hyp	Ref	Expression
1		fveqeq2	$⊢ w = W \to (\|w\| = N \leftrightarrow \|W\| = N)$
2	1	elrab	$⊢ W \in \{w \in Word V \| \|w\| = N\} \leftrightarrow (W \in Word V \land \|W\| = N)$
3		wrdnval	$⊢ (V \in X \land N \in ℕ_{0}) \to \{w \in Word V \| \|w\| = N\} = V^{(0 ..^N)}$
4	3	eleq2d	$⊢ (V \in X \land N \in ℕ_{0}) \to (W \in \{w \in Word V \| \|w\| = N\} \leftrightarrow W \in (V^{(0 ..^N)}))$
5	2 4	bitr3id	$⊢ (V \in X \land N \in ℕ_{0}) \to ((W \in Word V \land \|W\| = N) \leftrightarrow W \in (V^{(0 ..^N)}))$

Metamath Proof Explorer