Theorem ccatws1n0

Description: The concatenation of a word with a singleton word is not the empty set. (Contributed by Alexander van der Vekens, 29-Sep-2018) (Revised by AV, 5-Mar-2022)

	Ref	Expression
Assertion	ccatws1n0	$$⊢W\in \mathrm{Word}V\to W\mathrm{++}⟨“X”⟩\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		lencl	$$⊢W\in \mathrm{Word}V\to \left|W\right|\in {\mathbb{N}}_0$$
2		nn0p1gt0	$$⊢\left|W\right|\in {\mathbb{N}}_0\to 0<\left|W\right|+1$$
3	1 2	syl	$$⊢W\in \mathrm{Word}V\to 0<\left|W\right|+1$$
4		ccatws1len	$$⊢W\in \mathrm{Word}V\to \left|W\mathrm{++}⟨“X”⟩\right|=\left|W\right|+1$$
5	3 4	breqtrrd	$$⊢W\in \mathrm{Word}V\to 0<\left|W\mathrm{++}⟨“X”⟩\right|$$
6		ovex	$$⊢W\mathrm{++}⟨“X”⟩\in \mathrm{V}$$
7		hashneq0	$$⊢W\mathrm{++}⟨“X”⟩\in \mathrm{V}\to \left(0<\left|W\mathrm{++}⟨“X”⟩\right|\leftrightarrow W\mathrm{++}⟨“X”⟩\ne \varnothing \right)$$
8	6 7	ax-mp	$$⊢0<\left|W\mathrm{++}⟨“X”⟩\right|\leftrightarrow W\mathrm{++}⟨“X”⟩\ne \varnothing$$
9	5 8	sylib	$$⊢W\in \mathrm{Word}V\to W\mathrm{++}⟨“X”⟩\ne \varnothing$$