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	⊢ ..^ = ( 𝑚 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( 𝑚 ... ( 𝑛 − 1 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfzo	⊢ ..^
1		vm	⊢ 𝑚
2		cz	⊢ ℤ
3		vn	⊢ 𝑛
4	1	cv	⊢ 𝑚
5		cfz	⊢ ...
6	3	cv	⊢ 𝑛
7		cmin	⊢ −
8		c1	⊢ 1
9	6 8 7	co	⊢ ( 𝑛 − 1 )
10	4 9 5	co	⊢ ( 𝑚 ... ( 𝑛 − 1 ) )
11	1 3 2 2 10	cmpo	⊢ ( 𝑚 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( 𝑚 ... ( 𝑛 − 1 ) ) )
12	0 11	wceq	⊢ ..^ = ( 𝑚 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( 𝑚 ... ( 𝑛 − 1 ) ) )