Definition df-fzo

Description: Define a function generating sets of integers using ahalf-open range. Read ( M ..^ N ) as the integers from M up to, but not including, N ; contrast with ( M ... N ) df-fz , which includes N . Not including the endpoint simplifies a number of formulas related to cardinality and splitting; contrast fzosplit with fzsplit , for instance. (Contributed by Stefan O'Rear, 14-Aug-2015)

	Ref	Expression
Assertion	df-fzo	$$⊢..^=\left(m\in \mathbb{Z},n\in \mathbb{Z}⟼\left(m\dots n-1\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfzo	$$class..^$$
1		vm	$$setvarm$$
2		cz	$$class\mathbb{Z}$$
3		vn	$$setvarn$$
4	1	cv	$$setvarm$$
5		cfz	$$class\dots$$
6	3	cv	$$setvarn$$
7		cmin	$$class-$$
8		c1	$$class1$$
9	6 8 7	co	$$class\left(n-1\right)$$
10	4 9 5	co	$$class\left(m\dots n-1\right)$$
11	1 3 2 2 10	cmpo	$$class\left(m\in \mathbb{Z},n\in \mathbb{Z}⟼\left(m\dots n-1\right)\right)$$
12	0 11	wceq	$$wff..^=\left(m\in \mathbb{Z},n\in \mathbb{Z}⟼\left(m\dots n-1\right)\right)$$