Metamath Proof Explorer

Theorem lennncl

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

Ref Expression
Assertion lennncl ⊢ W ∈ Word S ∧ W ≠ ∅ → W ∈ ℕ

Proof

Step Hyp Ref Expression
1 wrdfin ⊢ W ∈ Word S → W ∈ Fin
2 hashnncl ⊢ W ∈ Fin → W ∈ ℕ ↔ W ≠ ∅
3 1 2 syl ⊢ W ∈ Word S → W ∈ ℕ ↔ W ≠ ∅
4 3 biimpar ⊢ W ∈ Word S ∧ W ≠ ∅ → W ∈ ℕ