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∈WordV∧W=N↔W∈V0..^N

Proof

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