Definition df-fz 8875

Description: Define an operation that produces a finite set of sequential integers. Read "𝑀...𝑁 " as "the set of integers from 𝑀 to 𝑁 inclusive." See fzval 8876 for its value and additional comments. (Contributed by NM, 6-Sep-2005.)

Assertion

Ref	Expression
df-fz	⊢ ... = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ (𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛)})

Distinct variable group:   𝑚,𝑛,𝑘

Detailed syntax breakdown of Definition df-fz

Step	Hyp	Ref	Expression
1		cfz 8874	. 2 class ...
2		vm	. . 3 setvar 𝑚
3		vn	. . 3 setvar 𝑛
4		cz 8245	. . 3 class ℤ
5	2	cv 1242	. . . . . 6 class 𝑚
6		vk	. . . . . . 7 setvar 𝑘
7	6	cv 1242	. . . . . 6 class 𝑘
8		cle 7061	. . . . . 6 class ≤
9	5, 7, 8	wbr 3764	. . . . 5 wff 𝑚 ≤ 𝑘
10	3	cv 1242	. . . . . 6 class 𝑛
11	7, 10, 8	wbr 3764	. . . . 5 wff 𝑘 ≤ 𝑛
12	9, 11	wa 97	. . . 4 wff (𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛)
13	12, 6, 4	crab 2310	. . 3 class {𝑘 ∈ ℤ ∣ (𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛)}
14	2, 3, 4, 4, 13	cmpt2 5514	. 2 class (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ (𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛)})
15	1, 14	wceq 1243	1 wff ... = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ (𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛)})

This definition is referenced by:  fzval  8876  fzf  8878  elfz2  8881