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 e. Word V -> ( W ++ <" X "> ) =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		lencl	|- ( W e. Word V -> ( # ` W ) e. NN0 )
2		nn0p1gt0	|- ( ( # ` W ) e. NN0 -> 0 < ( ( # ` W ) + 1 ) )
3	1 2	syl	|- ( W e. Word V -> 0 < ( ( # ` W ) + 1 ) )
4		ccatws1len	|- ( W e. Word V -> ( # ` ( W ++ <" X "> ) ) = ( ( # ` W ) + 1 ) )
5	3 4	breqtrrd	|- ( W e. Word V -> 0 < ( # ` ( W ++ <" X "> ) ) )
6		ovex	|- ( W ++ <" X "> ) e. _V
7		hashneq0	|- ( ( W ++ <" X "> ) e. _V -> ( 0 < ( # ` ( W ++ <" X "> ) ) <-> ( W ++ <" X "> ) =/= (/) ) )
8	6 7	ax-mp	|- ( 0 < ( # ` ( W ++ <" X "> ) ) <-> ( W ++ <" X "> ) =/= (/) )
9	5 8	sylib	|- ( W e. Word V -> ( W ++ <" X "> ) =/= (/) )