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 ( 𝑊 ∈ Word 𝑉 → ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ≠ ∅ )

Proof

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