Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-fzo Unicode version

Definition df-fzo 9101
 Description: Define a function generating sets of integers using a half-open range. Read ..^ as the integers from up to, but not including, ; contrast with df-fz 8976, which includes . Not including the endpoint simplifies a number of formulae related to cardinality and splitting; contrast fzosplit 9134 with fzsplit 9016, for instance. (Contributed by Stefan O'Rear, 14-Aug-2015.)
Assertion
Ref Expression
df-fzo ..^
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-fzo
StepHypRef Expression
1 cfzo 9100 . 2 ..^
2 vm . . 3
3 vn . . 3
4 cz 8301 . . 3
52cv 1258 . . . 4
63cv 1258 . . . . 5
7 c1 6947 . . . . 5
8 cmin 7244 . . . . 5
96, 7, 8co 5539 . . . 4
10 cfz 8975 . . . 4
115, 9, 10co 5539 . . 3
122, 3, 4, 4, 11cmpt2 5541 . 2
131, 12wceq 1259 1 ..^
 Colors of variables: wff set class This definition is referenced by:  fzof  9102  elfzoel1  9103  elfzoel2  9104  fzoval  9106
 Copyright terms: Public domain W3C validator