This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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