Metamath Proof Explorer

Theorem upwordsing

Description: Singleton is an increasing sequence for any compatible range. (Contributed by Ender Ting, 21-Nov-2024)

Ref Expression
Hypothesis upwordsing.1 ⊢ A ∈ S
Assertion upwordsing ⊢ ⟨“ A ”⟩ ∈ UpWord S

Proof

Step Hyp Ref Expression
1 upwordsing.1 ⊢ A ∈ S
2 s1cl ⊢ A ∈ S → ⟨“ A ”⟩ ∈ Word S
3 elab6g ⊢ ⟨“ A ”⟩ ∈ Word S → ⟨“ A ”⟩ ∈ w | w ∈ Word S ∧ ∀ k ∈ 0 ..^ w − 1 w ⁡ k < w ⁡ k + 1 ↔ ∀ w w = ⟨“ A ”⟩ → w ∈ Word S ∧ ∀ k ∈ 0 ..^ w − 1 w ⁡ k < w ⁡ k + 1
4 1 2 3 mp2b ⊢ ⟨“ A ”⟩ ∈ w | w ∈ Word S ∧ ∀ k ∈ 0 ..^ w − 1 w ⁡ k < w ⁡ k + 1 ↔ ∀ w w = ⟨“ A ”⟩ → w ∈ Word S ∧ ∀ k ∈ 0 ..^ w − 1 w ⁡ k < w ⁡ k + 1
5 eleq1a ⊢ ⟨“ A ”⟩ ∈ Word S → w = ⟨“ A ”⟩ → w ∈ Word S
6 1 2 5 mp2b ⊢ w = ⟨“ A ”⟩ → w ∈ Word S
7 fveq2 ⊢ w = ⟨“ A ”⟩ → w = ⟨“ A ”⟩
8 7 oveq1d ⊢ w = ⟨“ A ”⟩ → w − 1 = ⟨“ A ”⟩ − 1
9 s1len ⊢ ⟨“ A ”⟩ = 1
10 9 oveq1i ⊢ ⟨“ A ”⟩ − 1 = 1 − 1
11 1m1e0 ⊢ 1 − 1 = 0
12 10 11 eqtri ⊢ ⟨“ A ”⟩ − 1 = 0
13 8 12 eqtrdi ⊢ w = ⟨“ A ”⟩ → w − 1 = 0
14 13 oveq2d ⊢ w = ⟨“ A ”⟩ → 0 ..^ w − 1 = 0 ..^ 0
15 fzo0 ⊢ 0 ..^ 0 = ∅
16 14 15 eqtrdi ⊢ w = ⟨“ A ”⟩ → 0 ..^ w − 1 = ∅
17 rzal ⊢ 0 ..^ w − 1 = ∅ → ∀ k ∈ 0 ..^ w − 1 w ⁡ k < w ⁡ k + 1
18 16 17 syl ⊢ w = ⟨“ A ”⟩ → ∀ k ∈ 0 ..^ w − 1 w ⁡ k < w ⁡ k + 1
19 6 18 jca ⊢ w = ⟨“ A ”⟩ → w ∈ Word S ∧ ∀ k ∈ 0 ..^ w − 1 w ⁡ k < w ⁡ k + 1
20 4 19 mpgbir ⊢ ⟨“ A ”⟩ ∈ w | w ∈ Word S ∧ ∀ k ∈ 0 ..^ w − 1 w ⁡ k < w ⁡ k + 1
21 df-upword ⊢ UpWord S = w | w ∈ Word S ∧ ∀ k ∈ 0 ..^ w − 1 w ⁡ k < w ⁡ k + 1
22 20 21 eleqtrri ⊢ ⟨“ A ”⟩ ∈ UpWord S