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

Definition df-r1 9771
Description: Define the cumulative hierarchy of sets function, using Takeuti and Zaring's notation (𝑅1). It is also called the Von Neumann hierarchy of sets function. Starting with the empty set, this function builds up layers of sets where the next layer is the power set of the previous layer (and the union of all previous layers when the argument is a limit ordinal). Using the axiom of regularity, we can show that every set belongs to one of the layers of this hierarchy (see tz9.13 9801). Our definition expresses Definition 9.9 of [TakeutiZaring] p. 76 in a closed form, from which we derive the recursive definition as Theorems r10 9778, r1suc 9780, and r1lim 9782. Theorem r1val1 9796 shows a recursive definition that works for all values, and Theorems r1val2 9852 and r1val3 9853 show the value expressed in terms of rank.

Other notations for this function are R with the argument as a subscript (Equation 3.1 of [BellMachover] p. 477), V with a subscript (Definition of [Enderton] p. 202), M with a subscript (Definition 15.19 of [Monk1] p. 113), the capital Greek letter psi (Definition of [Mendelson] p. 281), and bold-face R (Definition 2.1 of [Kunen] p. 95).

The values of this function, that is, the layers of this hierarchy, are called "stages" to emphasize the process-like nature of this function. Some sources also use the term "level". (Contributed by NM, 2-Sep-2003.)

Assertion
Ref Expression
df-r1 𝑅1 = rec((𝑥 ∈ V ↦ 𝒫 𝑥), ∅)

Detailed syntax breakdown of Definition df-r1
StepHypRef Expression
1 cr1 9769 . 2 class 𝑅1
2 vx . . . 4 setvar 𝑥
3 cvv 3450 . . . 4 class V
42cv 1568 . . . . 5 class 𝑥
54cpw 4556 . . . 4 class 𝒫 𝑥
62, 3, 5cmpt 5185 . . 3 class (𝑥 ∈ V ↦ 𝒫 𝑥)
7 c0 4278 . . 3 class ∅
86, 7crdg 8420 . 2 class rec((𝑥 ∈ V ↦ 𝒫 𝑥), ∅)
91, 8wceq 1569 1 wff 𝑅1 = rec((𝑥 ∈ V ↦ 𝒫 𝑥), ∅)
Colors of variables:    wff setvar class
This definition is used by:  r1funlimOLD  9773  r1fun  9774  r1dmlim  9775  r1fnon  9776  r10  9778  r1sucg  9779  r1limg  9781
  Copyright terms: Public domain W3C validator