Theorem lennncl

Description: The length of a nonempty word is a positive integer. (Contributed by Mario Carneiro, 1-Oct-2015)

	Ref	Expression
Assertion	lennncl	⊢ ( ( 𝑊 ∈ Word 𝑆 ∧ 𝑊 ≠ ∅ ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		wrdfin	⊢ ( 𝑊 ∈ Word 𝑆 → 𝑊 ∈ Fin )
2		hashnncl	⊢ ( 𝑊 ∈ Fin → ( ( ♯ ‘ 𝑊 ) ∈ ℕ ↔ 𝑊 ≠ ∅ ) )
3	1 2	syl	⊢ ( 𝑊 ∈ Word 𝑆 → ( ( ♯ ‘ 𝑊 ) ∈ ℕ ↔ 𝑊 ≠ ∅ ) )
4	3	biimpar	⊢ ( ( 𝑊 ∈ Word 𝑆 ∧ 𝑊 ≠ ∅ ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )