Metamath Proof Explorer


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 ) ) )