Metamath Proof Explorer

Theorem upwordnul

Description: Empty set is an increasing sequence for every range. (Contributed by Ender Ting, 19-Nov-2024)

Ref Expression
Assertion upwordnul Could not format assertion : No typesetting found for |- (/) e. UpWord S with typecode |-

Proof

Step Hyp Ref Expression
1 0ex ⊢ ∅ ∈ V
2 elab6g ⊢ ∅ ∈ V → ∅ ∈ w | w ∈ Word S ∧ ∀ k ∈ 0 ..^ w − 1 w ⁡ k < w ⁡ k + 1 ↔ ∀ w w = ∅ → w ∈ Word S ∧ ∀ k ∈ 0 ..^ w − 1 w ⁡ k < w ⁡ k + 1
3 1 2 ax-mp ⊢ ∅ ∈ w | w ∈ Word S ∧ ∀ k ∈ 0 ..^ w − 1 w ⁡ k < w ⁡ k + 1 ↔ ∀ w w = ∅ → w ∈ Word S ∧ ∀ k ∈ 0 ..^ w − 1 w ⁡ k < w ⁡ k + 1
4 wrd0 ⊢ ∅ ∈ Word S
5 eleq1a ⊢ ∅ ∈ Word S → w = ∅ → w ∈ Word S
6 4 5 ax-mp ⊢ w = ∅ → w ∈ Word S
7 fveq2 ⊢ w = ∅ → w = ∅
8 hash0 ⊢ ∅ = 0
9 7 8 eqtrdi ⊢ w = ∅ → w = 0
10 9 oveq1d ⊢ w = ∅ → w − 1 = 0 − 1
11 0red ⊢ w = ∅ → 0 ∈ ℝ
12 11 lem1d ⊢ w = ∅ → 0 − 1 ≤ 0
13 10 12 eqbrtrd ⊢ w = ∅ → w − 1 ≤ 0
14 0z ⊢ 0 ∈ ℤ
15 9 14 eqeltrdi ⊢ w = ∅ → w ∈ ℤ
16 1zzd ⊢ w = ∅ → 1 ∈ ℤ
17 15 16 zsubcld ⊢ w = ∅ → w − 1 ∈ ℤ
18 fzon ⊢ 0 ∈ ℤ ∧ w − 1 ∈ ℤ → w − 1 ≤ 0 ↔ 0 ..^ w − 1 = ∅
19 14 17 18 sylancr ⊢ w = ∅ → w − 1 ≤ 0 ↔ 0 ..^ w − 1 = ∅
20 13 19 mpbid ⊢ w = ∅ → 0 ..^ w − 1 = ∅
21 rzal ⊢ 0 ..^ w − 1 = ∅ → ∀ k ∈ 0 ..^ w − 1 w ⁡ k < w ⁡ k + 1
22 20 21 syl ⊢ w = ∅ → ∀ k ∈ 0 ..^ w − 1 w ⁡ k < w ⁡ k + 1
23 6 22 jca ⊢ w = ∅ → w ∈ Word S ∧ ∀ k ∈ 0 ..^ w − 1 w ⁡ k < w ⁡ k + 1
24 3 23 mpgbir ⊢ ∅ ∈ w | w ∈ Word S ∧ ∀ k ∈ 0 ..^ w − 1 w ⁡ k < w ⁡ k + 1
25 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 |-
26 24 25 eleqtrri Could not format (/) e. UpWord S : No typesetting found for |- (/) e. UpWord S with typecode |-