Metamath Proof Explorer

Theorem iswrdsymb

Description: An arbitrary word is a word over an alphabet if all of its symbols belong to the alphabet. (Contributed by AV, 23-Jan-2021)

Ref Expression
Assertion iswrdsymb ⊢ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W W ⁡ i ∈ V → W ∈ Word V

Proof

Step Hyp Ref Expression
1 wrdfn ⊢ W ∈ Word V → W Fn 0 ..^ W
2 1 anim1i ⊢ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W W ⁡ i ∈ V → W Fn 0 ..^ W ∧ ∀ i ∈ 0 ..^ W W ⁡ i ∈ V
3 ffnfv ⊢ W : 0 ..^ W ⟶ V ↔ W Fn 0 ..^ W ∧ ∀ i ∈ 0 ..^ W W ⁡ i ∈ V
4 2 3 sylibr ⊢ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W W ⁡ i ∈ V → W : 0 ..^ W ⟶ V
5 iswrdi ⊢ W : 0 ..^ W ⟶ V → W ∈ Word V
6 4 5 syl ⊢ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W W ⁡ i ∈ V → W ∈ Word V