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 Could not format assertion : No typesetting found for |- <" A "> e. UpWord S with typecode |-

Proof

Step Hyp Ref Expression
1 upwordsing.1 ⊢A∈S
2 s1cl ⊢A∈S→⟨“A”⟩∈WordS
3 elab6g ⊢⟨“A”⟩∈WordS→⟨“A”⟩∈w|w∈WordS∧∀k∈0..^w−1w⁡k<w⁡k+1↔∀ww=⟨“A”⟩→w∈WordS∧∀k∈0..^w−1w⁡k<w⁡k+1
4 1 2 3 mp2b ⊢⟨“A”⟩∈w|w∈WordS∧∀k∈0..^w−1w⁡k<w⁡k+1↔∀ww=⟨“A”⟩→w∈WordS∧∀k∈0..^w−1w⁡k<w⁡k+1
5 eleq1a ⊢⟨“A”⟩∈WordS→w=⟨“A”⟩→w∈WordS
6 1 2 5 mp2b ⊢w=⟨“A”⟩→w∈WordS
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−1w⁡k<w⁡k+1
18 16 17 syl ⊢w=⟨“A”⟩→∀k∈0..^w−1w⁡k<w⁡k+1
19 6 18 jca ⊢w=⟨“A”⟩→w∈WordS∧∀k∈0..^w−1w⁡k<w⁡k+1
20 4 19 mpgbir ⊢⟨“A”⟩∈w|w∈WordS∧∀k∈0..^w−1w⁡k<w⁡k+1
21 df-upword Could not format UpWord S = { w | ( w e. Word S /\ A. k e. ( 0 ..^ ( ( # ` w ) - 1 ) ) ( w ` k ) < ( w ` ( k + 1 ) ) ) } : No typesetting found for |- UpWord S = { w | ( w e. Word S /\ A. k e. ( 0 ..^ ( ( # ` w ) - 1 ) ) ( w ` k ) < ( w ` ( k + 1 ) ) ) } with typecode |-
22 20 21 eleqtrri Could not format <" A "> e. UpWord S : No typesetting found for |- <" A "> e. UpWord S with typecode |-