Database
REAL AND COMPLEX NUMBERS
Words over a set
Definitions and basic theorems
wrdsymb
Next ⟩
nfwrd
Metamath Proof Explorer
Ascii
Unicode
Theorem
wrdsymb
Description:
A word is a word over the symbols it consists of.
(Contributed by
AV
, 1-Dec-2022)
Ref
Expression
Assertion
wrdsymb
⊢
S
∈
Word
A
→
S
∈
Word
S
0
..^
S
Proof
Step
Hyp
Ref
Expression
1
wrdf
⊢
S
∈
Word
A
→
S
:
0
..^
S
⟶
A
2
fimadmfo
⊢
S
:
0
..^
S
⟶
A
→
S
:
0
..^
S
⟶
onto
S
0
..^
S
3
fof
⊢
S
:
0
..^
S
⟶
onto
S
0
..^
S
→
S
:
0
..^
S
⟶
S
0
..^
S
4
1
2
3
3syl
⊢
S
∈
Word
A
→
S
:
0
..^
S
⟶
S
0
..^
S
5
iswrdb
⊢
S
∈
Word
S
0
..^
S
↔
S
:
0
..^
S
⟶
S
0
..^
S
6
4
5
sylibr
⊢
S
∈
Word
A
→
S
∈
Word
S
0
..^
S