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,nk|mkkn

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfz class
1 vm setvarm
2 cz class
3 vn setvarn
4 vk setvark
5 1 cv setvarm
6 cle class
7 4 cv setvark
8 5 7 6 wbr wffmk
9 3 cv setvarn
10 7 9 6 wbr wffkn
11 8 10 wa wffmkkn
12 11 4 2 crab classk|mkkn
13 1 3 2 2 12 cmpo classm,nk|mkkn
14 0 13 wceq wff=m,nk|mkkn