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

Definition df-r1 9028
 Description: Define the cumulative hierarchy of sets function, using Takeuti and Zaring's notation (𝑅1). 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 previous layers when the argument is a limit ordinal). Using the Axiom of Regularity, we can show that any set whatsoever belongs to one of the layers of this hierarchy (see tz9.13 9055). Our definition expresses Definition 9.9 of [TakeutiZaring] p. 76 in a closed form, from which we derive the recursive definition as theorems r10 9032, r1suc 9034, and r1lim 9036. Theorem r1val1 9050 shows a recursive definition that works for all values, and theorems r1val2 9101 and r1val3 9102 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). (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 9026 . 2 class 𝑅1
2 vx . . . 4 setvar 𝑥
3 cvv 3432 . . . 4 class V
42cv 1519 . . . . 5 class 𝑥
54cpw 4447 . . . 4 class 𝒫 𝑥
62, 3, 5cmpt 5035 . . 3 class (𝑥 ∈ V ↦ 𝒫 𝑥)
7 c0 4206 . . 3 class
86, 7crdg 7888 . 2 class rec((𝑥 ∈ V ↦ 𝒫 𝑥), ∅)
91, 8wceq 1520 1 wff 𝑅1 = rec((𝑥 ∈ V ↦ 𝒫 𝑥), ∅)
 Colors of variables: wff setvar class This definition is referenced by:  r1funlim  9030  r1fnon  9031  r10  9032  r1sucg  9033  r1limg  9035
 Copyright terms: Public domain W3C validator