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 ∈ Word V → W ++ ⟨“ X ”⟩ ≠ ∅

Proof

Step Hyp Ref Expression
1 lencl ⊢ W ∈ Word V → W ∈ ℕ 0
2 nn0p1gt0 ⊢ W ∈ ℕ 0 → 0 < W + 1
3 1 2 syl ⊢ W ∈ Word V → 0 < W + 1
4 ccatws1len ⊢ W ∈ Word V → W ++ ⟨“ X ”⟩ = W + 1
5 3 4 breqtrrd ⊢ W ∈ Word V → 0 < W ++ ⟨“ X ”⟩
6 ovex ⊢ W ++ ⟨“ X ”⟩ ∈ V
7 hashneq0 ⊢ W ++ ⟨“ X ”⟩ ∈ V → 0 < W ++ ⟨“ X ”⟩ ↔ W ++ ⟨“ X ”⟩ ≠ ∅
8 6 7 ax-mp ⊢ 0 < W ++ ⟨“ X ”⟩ ↔ W ++ ⟨“ X ”⟩ ≠ ∅
9 5 8 sylib ⊢ W ∈ Word V → W ++ ⟨“ X ”⟩ ≠ ∅