Definition df-fz 10101

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 10102 for its value and additional comments. (Contributed by NM, 6-Sep-2005.)

Assertion

Ref	Expression
df-fz	|- ... = ( m e. ZZ , n e. ZZ |-> { k e. ZZ | ( m <_ k /\ k <_ n ) } )

Distinct variable group:   m, n, k

Detailed syntax breakdown of Definition df-fz

Step	Hyp	Ref	Expression
1		cfz 10100	. 2 class ...
2		vm	. . 3 setvar m
3		vn	. . 3 setvar n
4		cz 9343	. . 3 class ZZ
5	2	cv 1363	. . . . . 6 class m
6		vk	. . . . . . 7 setvar k
7	6	cv 1363	. . . . . 6 class k
8		cle 8079	. . . . . 6 class <_
9	5, 7, 8	wbr 4034	. . . . 5 wff m <_ k
10	3	cv 1363	. . . . . 6 class n
11	7, 10, 8	wbr 4034	. . . . 5 wff k <_ n
12	9, 11	wa 104	. . . 4 wff ( m <_ k /\ k <_ n )
13	12, 6, 4	crab 2479	. . 3 class { k e. ZZ | ( m <_ k /\ k <_ n ) }
14	2, 3, 4, 4, 13	cmpo 5927	. 2 class ( m e. ZZ , n e. ZZ |-> { k e. ZZ | ( m <_ k /\ k <_ n ) } )
15	1, 14	wceq 1364	1 wff ... = ( m e. ZZ , n e. ZZ |-> { k e. ZZ | ( m <_ k /\ k <_ n ) } )

This definition is referenced by:  fzval  10102  fzf  10104  elfz2  10107