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 e. ZZ , n e. ZZ |-> { k e. ZZ | ( m <_ k /\ k <_ n ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfz	|- ...
1		vm	|- m
2		cz	|- ZZ
3		vn	|- n
4		vk	|- k
5	1	cv	|- m
6		cle	|- <_
7	4	cv	|- k
8	5 7 6	wbr	|- m <_ k
9	3	cv	|- n
10	7 9 6	wbr	|- k <_ n
11	8 10	wa	|- ( m <_ k /\ k <_ n )
12	11 4 2	crab	|- { k e. ZZ | ( m <_ k /\ k <_ n ) }
13	1 3 2 2 12	cmpo	|- ( m e. ZZ , n e. ZZ |-> { k e. ZZ | ( m <_ k /\ k <_ n ) } )
14	0 13	wceq	|- ... = ( m e. ZZ , n e. ZZ |-> { k e. ZZ | ( m <_ k /\ k <_ n ) } )