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