Theorem singoutnword

Description: Singleton with character out of range V is not a word for that range. (Contributed by Ender Ting, 21-Nov-2024)

	Ref	Expression
Hypothesis	singoutnword.1	$$⊢A\in \mathrm{V}$$
Assertion	singoutnword	$$⊢\neg A\in V\to \neg ⟨“A”⟩\in \mathrm{Word}V$$

Proof

Step	Hyp	Ref	Expression
1		singoutnword.1	$$⊢A\in \mathrm{V}$$
2		s1fv	$$⊢A\in \mathrm{V}\to ⟨“A”⟩\left(0\right)=A$$
3	1 2	ax-mp	$$⊢⟨“A”⟩\left(0\right)=A$$
4		s1nz	$$⊢⟨“A”⟩\ne \varnothing$$
5		fstwrdne	$$⊢\left(⟨“A”⟩\in \mathrm{Word}V\wedge ⟨“A”⟩\ne \varnothing \right)\to ⟨“A”⟩\left(0\right)\in V$$
6	4 5	mpan2	$$⊢⟨“A”⟩\in \mathrm{Word}V\to ⟨“A”⟩\left(0\right)\in V$$
7	3 6	eqeltrrid	$$⊢⟨“A”⟩\in \mathrm{Word}V\to A\in V$$
8	7	con3i	$$⊢\neg A\in V\to \neg ⟨“A”⟩\in \mathrm{Word}V$$