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

Definition df-uz 11880
Description: Define a function whose value at 𝑗 is the semi-infinite set of contiguous integers starting at 𝑗, which we will also call the upper integers starting at 𝑗. Read "𝑀 " as "the set of integers greater than or equal to 𝑀." See uzval 11881 for its value, uzssz 11899 for its relationship to , nnuz 11916 and nn0uz 11915 for its relationships to and 0, and eluz1 11883 and eluz2 11885 for its membership relations. (Contributed by NM, 5-Sep-2005.)
Assertion
Ref Expression
df-uz = (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗𝑘})
Distinct variable group:   𝑗,𝑘

Detailed syntax breakdown of Definition df-uz
StepHypRef Expression
1 cuz 11879 . 2 class
2 vj . . 3 setvar 𝑗
3 cz 11569 . . 3 class
42cv 1631 . . . . 5 class 𝑗
5 vk . . . . . 6 setvar 𝑘
65cv 1631 . . . . 5 class 𝑘
7 cle 10267 . . . . 5 class
84, 6, 7wbr 4804 . . . 4 wff 𝑗𝑘
98, 5, 3crab 3054 . . 3 class {𝑘 ∈ ℤ ∣ 𝑗𝑘}
102, 3, 9cmpt 4881 . 2 class (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗𝑘})
111, 10wceq 1632 1 wff = (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗𝑘})
Colors of variables: wff setvar class
This definition is referenced by:  uzval  11881  uzf  11882
  Copyright terms: Public domain W3C validator