Metamath Proof Explorer


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 "> ) =/= (/) )