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∈WordV∧∀i∈0..^WW⁡i∈V→W∈WordV

Proof

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