Definition df-fz 7638

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 7639 for its value and additional comments.

Assertion

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

Distinct variable group:   m,n,k,z

Detailed syntax breakdown of Definition df-fz

Step	Hyp	Ref	Expression
1		cfz 7637	. 2 class ...
2		vm	. . . . . . 7 set m
3	2	cv 1297	. . . . . 6 class m
4		cz 6451	. . . . . 6 class ZZ
5	3, 4	wcel 1300	. . . . 5 wff m e. ZZ
6		vn	. . . . . . 7 set n
7	6	cv 1297	. . . . . 6 class n
8	7, 4	wcel 1300	. . . . 5 wff n e. ZZ
9	5, 8	wa 240	. . . 4 wff (m e. ZZ /\ n e. ZZ)
10		vz	. . . . . 6 set z
11	10	cv 1297	. . . . 5 class z
12		vk	. . . . . . . . 9 set k
13	12	cv 1297	. . . . . . . 8 class k
14		cle 6448	. . . . . . . 8 class <_
15	3, 13, 14	wbr 3338	. . . . . . 7 wff m <_ k
16	13, 7, 14	wbr 3338	. . . . . . 7 wff k <_ n
17	15, 16	wa 240	. . . . . 6 wff (m <_ k /\ k <_ n)
18	17, 12, 4	crab 2108	. . . . 5 class {k e. ZZ | (m <_ k /\ k <_ n)}
19	11, 18	wceq 1298	. . . 4 wff z = {k e. ZZ | (m <_ k /\ k <_ n)}
20	9, 19	wa 240	. . 3 wff ((m e. ZZ /\ n e. ZZ) /\ z = {k e. ZZ | (m <_ k /\ k <_ n)})
21	20, 2, 6, 10	copab2 4885	. 2 class {<.<.m, n>., z>. | ((m e. ZZ /\ n e. ZZ) /\ z = {k e. ZZ | (m <_ k /\ k <_ n)})}
22	1, 21	wceq 1298	1 wff ... = {<.<.m, n>., z>. | ((m e. ZZ /\ n e. ZZ) /\ z = {k e. ZZ | (m <_ k /\ k <_ n)})}

This definition is referenced by:  fzval 7639  elfz2 7642  elfzlem 7643

Copyright terms: Public domain