Metamath Proof Explorer

Theorem wrdmap

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

Ref Expression
Assertion wrdmap ⊢ V ∈ X ∧ N ∈ ℕ 0 → W ∈ Word V ∧ W = N ↔ W ∈ V 0 ..^ N

Proof

Step Hyp Ref Expression
1 fveqeq2 ⊢ w = W → w = N ↔ W = N
2 1 elrab ⊢ W ∈ w ∈ Word V | w = N ↔ W ∈ Word V ∧ W = N
3 wrdnval ⊢ V ∈ X ∧ N ∈ ℕ 0 → w ∈ Word V | w = N = V 0 ..^ N
4 3 eleq2d ⊢ V ∈ X ∧ N ∈ ℕ 0 → W ∈ w ∈ Word V | w = N ↔ W ∈ V 0 ..^ N
5 2 4 bitr3id ⊢ V ∈ X ∧ N ∈ ℕ 0 → W ∈ Word V ∧ W = N ↔ W ∈ V 0 ..^ N