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