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 ( ( 𝑊 ∈ Word V ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ∈ 𝑉 ) → 𝑊 ∈ Word 𝑉 )

Proof

Step Hyp Ref Expression
1 wrdfn ( 𝑊 ∈ Word V → 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
2 1 anim1i ( ( 𝑊 ∈ Word V ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ∈ 𝑉 ) → ( 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ∈ 𝑉 ) )
3 ffnfv ( 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑉 ↔ ( 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ∈ 𝑉 ) )
4 2 3 sylibr ( ( 𝑊 ∈ Word V ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ∈ 𝑉 ) → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑉 )
5 iswrdi ( 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑉𝑊 ∈ Word 𝑉 )
6 4 5 syl ( ( 𝑊 ∈ Word V ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) ∈ 𝑉 ) → 𝑊 ∈ Word 𝑉 )