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 ∈ X ∧ N ∈ ℕ 0 → w ∈ Word V | w = N = V 0 ..^ N

Proof

Step Hyp Ref Expression
1 df-rab ⊢ w ∈ Word V | w = N = w | w ∈ Word V ∧ w = N
2 ovexd ⊢ V ∈ X ∧ N ∈ ℕ 0 → 0 ..^ N ∈ V
3 elmapg ⊢ V ∈ X ∧ 0 ..^ N ∈ V → w ∈ V 0 ..^ N ↔ w : 0 ..^ N ⟶ V
4 2 3 syldan ⊢ V ∈ X ∧ N ∈ ℕ 0 → w ∈ V 0 ..^ N ↔ w : 0 ..^ N ⟶ V
5 iswrdi ⊢ w : 0 ..^ N ⟶ V → w ∈ Word V
6 5 adantl ⊢ V ∈ X ∧ N ∈ ℕ 0 ∧ w : 0 ..^ N ⟶ V → w ∈ Word V
7 fnfzo0hash ⊢ N ∈ ℕ 0 ∧ w : 0 ..^ N ⟶ V → w = N
8 7 adantll ⊢ V ∈ X ∧ N ∈ ℕ 0 ∧ w : 0 ..^ N ⟶ V → w = N
9 6 8 jca ⊢ V ∈ X ∧ N ∈ ℕ 0 ∧ w : 0 ..^ N ⟶ V → w ∈ Word V ∧ w = N
10 9 ex ⊢ V ∈ X ∧ N ∈ ℕ 0 → w : 0 ..^ N ⟶ V → w ∈ Word V ∧ w = N
11 wrdf ⊢ w ∈ Word V → w : 0 ..^ w ⟶ V
12 oveq2 ⊢ w = N → 0 ..^ w = 0 ..^ N
13 12 feq2d ⊢ w = N → w : 0 ..^ w ⟶ V ↔ w : 0 ..^ N ⟶ V
14 11 13 syl5ibcom ⊢ w ∈ Word V → w = N → w : 0 ..^ N ⟶ V
15 14 imp ⊢ w ∈ Word V ∧ w = N → w : 0 ..^ N ⟶ V
16 10 15 impbid1 ⊢ V ∈ X ∧ N ∈ ℕ 0 → w : 0 ..^ N ⟶ V ↔ w ∈ Word V ∧ w = N
17 4 16 bitrd ⊢ V ∈ X ∧ N ∈ ℕ 0 → w ∈ V 0 ..^ N ↔ w ∈ Word V ∧ w = N
18 17 eqabdv ⊢ V ∈ X ∧ N ∈ ℕ 0 → V 0 ..^ N = w | w ∈ Word V ∧ w = N
19 1 18 eqtr4id ⊢ V ∈ X ∧ N ∈ ℕ 0 → w ∈ Word V | w = N = V 0 ..^ N