MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-fz Structured version   Visualization version   GIF version

Definition df-fz 12155
Description: Define an operation that produces a finite set of sequential integers. Read "𝑀...𝑁 " as "the set of integers from 𝑀 to 𝑁 inclusive." See fzval 12156 for its value and additional comments. (Contributed by NM, 6-Sep-2005.)
Assertion
Ref Expression
df-fz ... = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ (𝑚𝑘𝑘𝑛)})
Distinct variable group:   𝑚,𝑛,𝑘

Detailed syntax breakdown of Definition df-fz
StepHypRef Expression
1 cfz 12154 . 2 class ...
2 vm . . 3 setvar 𝑚
3 vn . . 3 setvar 𝑛
4 cz 11212 . . 3 class
52cv 1473 . . . . . 6 class 𝑚
6 vk . . . . . . 7 setvar 𝑘
76cv 1473 . . . . . 6 class 𝑘
8 cle 9931 . . . . . 6 class
95, 7, 8wbr 4577 . . . . 5 wff 𝑚𝑘
103cv 1473 . . . . . 6 class 𝑛
117, 10, 8wbr 4577 . . . . 5 wff 𝑘𝑛
129, 11wa 382 . . . 4 wff (𝑚𝑘𝑘𝑛)
1312, 6, 4crab 2899 . . 3 class {𝑘 ∈ ℤ ∣ (𝑚𝑘𝑘𝑛)}
142, 3, 4, 4, 13cmpt2 6528 . 2 class (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ (𝑚𝑘𝑘𝑛)})
151, 14wceq 1474 1 wff ... = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ (𝑚𝑘𝑘𝑛)})
Colors of variables: wff setvar class
This definition is referenced by:  fzval  12156  fzf  12158
  Copyright terms: Public domain W3C validator