Definition df-fz 6468

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 fzvalt 6469 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 6467	. 2 class ...
2		vm	. . . . . . 7 set m
3	2	cv 955	. . . . . 6 class m
4		cz 5298	. . . . . 6 class ZZ
5	3, 4	wcel 958	. . . . 5 wff m e. ZZ
6		vn	. . . . . . 7 set n
7	6	cv 955	. . . . . 6 class n
8	7, 4	wcel 958	. . . . 5 wff n e. ZZ
9	5, 8	wa 223	. . . 4 wff (m e. ZZ /\ n e. ZZ)
10		vz	. . . . . 6 set z
11	10	cv 955	. . . . 5 class z
12		vk	. . . . . . . . 9 set k
13	12	cv 955	. . . . . . . 8 class k
14		cle 5295	. . . . . . . 8 class <_
15	3, 13, 14	wbr 2619	. . . . . . 7 wff m <_ k
16	13, 7, 14	wbr 2619	. . . . . . 7 wff k <_ n
17	15, 16	wa 223	. . . . . 6 wff (m <_ k /\ k <_ n)
18	17, 12, 4	crab 1648	. . . . 5 class {k e. ZZ | (m <_ k /\ k <_ n)}
19	11, 18	wceq 956	. . . 4 wff z = {k e. ZZ | (m <_ k /\ k <_ n)}
20	9, 19	wa 223	. . 3 wff ((m e. ZZ /\ n e. ZZ) /\ z = {k e. ZZ | (m <_ k /\ k <_ n)})
21	20, 2, 6, 10	copab2 3964	. 2 class {<.<.m, n>., z>. | ((m e. ZZ /\ n e. ZZ) /\ z = {k e. ZZ | (m <_ k /\ k <_ n)})}
22	1, 21	wceq 956	1 wff ... = {<.<.m, n>., z>. | ((m e. ZZ /\ n e. ZZ) /\ z = {k e. ZZ | (m <_ k /\ k <_ n)})}

This definition is referenced by:  fzvalt 6469  elfz2t 6472  elfzlem 6473

Copyright terms: Public domain