Metamath Proof Explorer


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