wrdsymb

Description: A word is a word over the symbols it consists of. (Contributed by AV, 1-Dec-2022)

		Ref	Expression
	Assertion	wrdsymb	$⊢ S \in Word A \to S \in Word S [(0 ..^\|S\|)]$

Step	Hyp	Ref	Expression
1		wrdf	$⊢ S \in Word A \to S : (0 ..^\|S\|) ⟶ A$
2		fimadmfo	$⊢ S : (0 ..^\|S\|) ⟶ A \to S : (0 ..^\|S\|) \underset{onto}{⟶} S [(0 ..^\|S\|)]$
3		fof	$⊢ S : (0 ..^\|S\|) \underset{onto}{⟶} S [(0 ..^\|S\|)] \to S : (0 ..^\|S\|) ⟶ S [(0 ..^\|S\|)]$
4	1 2 3	3syl	$⊢ S \in Word A \to S : (0 ..^\|S\|) ⟶ S [(0 ..^\|S\|)]$
5		iswrdb	$⊢ S \in Word S [(0 ..^\|S\|)] \leftrightarrow S : (0 ..^\|S\|) ⟶ S [(0 ..^\|S\|)]$
6	4 5	sylibr	$⊢ S \in Word A \to S \in Word S [(0 ..^\|S\|)]$

Metamath Proof Explorer