Theorem upwordnul

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

	Ref	Expression
Assertion	upwordnul	⊢ ∅ ∈ UpWord 𝑆

Proof

Step	Hyp	Ref	Expression
1		0ex	⊢ ∅ ∈ V
2		elab6g	⊢ ( ∅ ∈ V → ( ∅ ∈ { 𝑤 ∣ ( 𝑤 ∈ Word 𝑆 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) ( 𝑤 ‘ 𝑘 ) < ( 𝑤 ‘ ( 𝑘 + 1 ) ) ) } ↔ ∀ 𝑤 ( 𝑤 = ∅ → ( 𝑤 ∈ Word 𝑆 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) ( 𝑤 ‘ 𝑘 ) < ( 𝑤 ‘ ( 𝑘 + 1 ) ) ) ) ) )
3	1 2	ax-mp	⊢ ( ∅ ∈ { 𝑤 ∣ ( 𝑤 ∈ Word 𝑆 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) ( 𝑤 ‘ 𝑘 ) < ( 𝑤 ‘ ( 𝑘 + 1 ) ) ) } ↔ ∀ 𝑤 ( 𝑤 = ∅ → ( 𝑤 ∈ Word 𝑆 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) ( 𝑤 ‘ 𝑘 ) < ( 𝑤 ‘ ( 𝑘 + 1 ) ) ) ) )
4		wrd0	⊢ ∅ ∈ Word 𝑆
5		eleq1a	⊢ ( ∅ ∈ Word 𝑆 → ( 𝑤 = ∅ → 𝑤 ∈ Word 𝑆 ) )
6	4 5	ax-mp	⊢ ( 𝑤 = ∅ → 𝑤 ∈ Word 𝑆 )
7		fveq2	⊢ ( 𝑤 = ∅ → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ ∅ ) )
8		hash0	⊢ ( ♯ ‘ ∅ ) = 0
9	7 8	eqtrdi	⊢ ( 𝑤 = ∅ → ( ♯ ‘ 𝑤 ) = 0 )
10	9	oveq1d	⊢ ( 𝑤 = ∅ → ( ( ♯ ‘ 𝑤 ) − 1 ) = ( 0 − 1 ) )
11		0red	⊢ ( 𝑤 = ∅ → 0 ∈ ℝ )
12	11	lem1d	⊢ ( 𝑤 = ∅ → ( 0 − 1 ) ≤ 0 )
13	10 12	eqbrtrd	⊢ ( 𝑤 = ∅ → ( ( ♯ ‘ 𝑤 ) − 1 ) ≤ 0 )
14		0z	⊢ 0 ∈ ℤ
15	9 14	eqeltrdi	⊢ ( 𝑤 = ∅ → ( ♯ ‘ 𝑤 ) ∈ ℤ )
16		1zzd	⊢ ( 𝑤 = ∅ → 1 ∈ ℤ )
17	15 16	zsubcld	⊢ ( 𝑤 = ∅ → ( ( ♯ ‘ 𝑤 ) − 1 ) ∈ ℤ )
18		fzon	⊢ ( ( 0 ∈ ℤ ∧ ( ( ♯ ‘ 𝑤 ) − 1 ) ∈ ℤ ) → ( ( ( ♯ ‘ 𝑤 ) − 1 ) ≤ 0 ↔ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) = ∅ ) )
19	14 17 18	sylancr	⊢ ( 𝑤 = ∅ → ( ( ( ♯ ‘ 𝑤 ) − 1 ) ≤ 0 ↔ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) = ∅ ) )
20	13 19	mpbid	⊢ ( 𝑤 = ∅ → ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) = ∅ )
21		rzal	⊢ ( ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) = ∅ → ∀ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) ( 𝑤 ‘ 𝑘 ) < ( 𝑤 ‘ ( 𝑘 + 1 ) ) )
22	20 21	syl	⊢ ( 𝑤 = ∅ → ∀ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) ( 𝑤 ‘ 𝑘 ) < ( 𝑤 ‘ ( 𝑘 + 1 ) ) )
23	6 22	jca	⊢ ( 𝑤 = ∅ → ( 𝑤 ∈ Word 𝑆 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) ( 𝑤 ‘ 𝑘 ) < ( 𝑤 ‘ ( 𝑘 + 1 ) ) ) )
24	3 23	mpgbir	⊢ ∅ ∈ { 𝑤 ∣ ( 𝑤 ∈ Word 𝑆 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) ( 𝑤 ‘ 𝑘 ) < ( 𝑤 ‘ ( 𝑘 + 1 ) ) ) }
25		df-upword	⊢ UpWord 𝑆 = { 𝑤 ∣ ( 𝑤 ∈ Word 𝑆 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) ( 𝑤 ‘ 𝑘 ) < ( 𝑤 ‘ ( 𝑘 + 1 ) ) ) }
26	24 25	eleqtrri	⊢ ∅ ∈ UpWord 𝑆