Metamath Proof Explorer

Definition df-fz

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

Ref Expression
Assertion df-fz ⊢ … = m ∈ ℤ , n ∈ ℤ ⟼ k ∈ ℤ | m ≤ k ∧ k ≤ n

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfz class …
1 vm setvar m
2 cz class ℤ
3 vn setvar n
4 vk setvar k
5 1 cv setvar m
6 cle class ≤
7 4 cv setvar k
8 5 7 6 wbr wff m ≤ k
9 3 cv setvar n
10 7 9 6 wbr wff k ≤ n
11 8 10 wa wff m ≤ k ∧ k ≤ n
12 11 4 2 crab class k ∈ ℤ | m ≤ k ∧ k ≤ n
13 1 3 2 2 12 cmpo class m ∈ ℤ , n ∈ ℤ ⟼ k ∈ ℤ | m ≤ k ∧ k ≤ n
14 0 13 wceq wff … = m ∈ ℤ , n ∈ ℤ ⟼ k ∈ ℤ | m ≤ k ∧ k ≤ n