Theorem upwordsing

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

	Ref	Expression
Hypothesis	upwordsing.1	⊢ 𝐴 ∈ 𝑆
Assertion	upwordsing	⊢ ⟨“ 𝐴 ”⟩ ∈ UpWord 𝑆

Proof

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