This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝑉 )