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