Metamath Proof Explorer

Theorem upwordisword

Description: Any increasing sequence is a sequence. (Contributed by Ender Ting, 19-Nov-2024)

Ref Expression
Assertion upwordisword ⊢ A ∈ UpWord S → A ∈ Word S

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ w = A → w ∈ Word S ↔ A ∈ Word S
2 df-upword ⊢ UpWord S = w | w ∈ Word S ∧ ∀ k ∈ 0 ..^ w − 1 w ⁡ k < w ⁡ k + 1
3 2 eqabri ⊢ w ∈ UpWord S ↔ w ∈ Word S ∧ ∀ k ∈ 0 ..^ w − 1 w ⁡ k < w ⁡ k + 1
4 3 simplbi ⊢ w ∈ UpWord S → w ∈ Word S
5 1 4 vtoclga ⊢ A ∈ UpWord S → A ∈ Word S