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∈WordS∧∀k∈0..^w−1w⁡k<w⁡k+1↔∀ww=∅→w∈WordS∧∀k∈0..^w−1w⁡k<w⁡k+1
3 1 2 ax-mp ⊢∅∈w|w∈WordS∧∀k∈0..^w−1w⁡k<w⁡k+1↔∀ww=∅→w∈WordS∧∀k∈0..^w−1w⁡k<w⁡k+1
4 wrd0 ⊢∅∈WordS
5 eleq1a ⊢∅∈WordS→w=∅→w∈WordS
6 4 5 ax-mp ⊢w=∅→w∈WordS
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−1w⁡k<w⁡k+1
22 20 21 syl ⊢w=∅→∀k∈0..^w−1w⁡k<w⁡k+1
23 6 22 jca ⊢w=∅→w∈WordS∧∀k∈0..^w−1w⁡k<w⁡k+1
24 3 23 mpgbir ⊢∅∈w|w∈WordS∧∀k∈0..^w−1w⁡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 |-