Metamath Proof Explorer

Theorem wrdnval

Description: Words of a fixed length are mappings from a fixed half-open integer interval. (Contributed by Alexander van der Vekens, 25-Mar-2018) (Proof shortened by AV, 13-May-2020)

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

Proof

Step	Hyp	Ref	Expression
1		df-rab	$⊢ \{w \in Word V \| \|w\| = N\} = \{w \| (w \in Word V \land \|w\| = N)\}$
2		ovexd	$⊢ (V \in X \land N \in ℕ_{0}) \to (0 ..^N) \in V$
3		elmapg	$⊢ (V \in X \land (0 ..^N) \in V) \to (w \in (V^{(0 ..^N)}) \leftrightarrow w : (0 ..^N) ⟶ V)$
4	2 3	syldan	$⊢ (V \in X \land N \in ℕ_{0}) \to (w \in (V^{(0 ..^N)}) \leftrightarrow w : (0 ..^N) ⟶ V)$
5		iswrdi	$⊢ w : (0 ..^N) ⟶ V \to w \in Word V$
6	5	adantl	$⊢ ((V \in X \land N \in ℕ_{0}) \land w : (0 ..^N) ⟶ V) \to w \in Word V$
7		fnfzo0hash	$⊢ (N \in ℕ_{0} \land w : (0 ..^N) ⟶ V) \to \|w\| = N$
8	7	adantll	$⊢ ((V \in X \land N \in ℕ_{0}) \land w : (0 ..^N) ⟶ V) \to \|w\| = N$
9	6 8	jca	$⊢ ((V \in X \land N \in ℕ_{0}) \land w : (0 ..^N) ⟶ V) \to (w \in Word V \land \|w\| = N)$
10	9	ex	$⊢ (V \in X \land N \in ℕ_{0}) \to (w : (0 ..^N) ⟶ V \to (w \in Word V \land \|w\| = N))$
11		wrdf	$⊢ w \in Word V \to w : (0 ..^\|w\|) ⟶ V$
12		oveq2	$⊢ \|w\| = N \to (0 ..^\|w\|) = (0 ..^N)$
13	12	feq2d	$⊢ \|w\| = N \to (w : (0 ..^\|w\|) ⟶ V \leftrightarrow w : (0 ..^N) ⟶ V)$
14	11 13	syl5ibcom	$⊢ w \in Word V \to (\|w\| = N \to w : (0 ..^N) ⟶ V)$
15	14	imp	$⊢ (w \in Word V \land \|w\| = N) \to w : (0 ..^N) ⟶ V$
16	10 15	impbid1	$⊢ (V \in X \land N \in ℕ_{0}) \to (w : (0 ..^N) ⟶ V \leftrightarrow (w \in Word V \land \|w\| = N))$
17	4 16	bitrd	$⊢ (V \in X \land N \in ℕ_{0}) \to (w \in (V^{(0 ..^N)}) \leftrightarrow (w \in Word V \land \|w\| = N))$
18	17	eqabdv	$⊢ (V \in X \land N \in ℕ_{0}) \to V^{(0 ..^N)} = \{w \| (w \in Word V \land \|w\| = N)\}$
19	1 18	eqtr4id	$⊢ (V \in X \land N \in ℕ_{0}) \to \{w \in Word V \| \|w\| = N\} = V^{(0 ..^N)}$