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

Definition df-r1 7320
Description: Define the cumulative hierarchy of sets function, using Takeuti and Zaring's notation ( R1). 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 7347). Our definition expresses Definition 9.9 of [TakeutiZaring] p. 76 in a closed form, from which we derive the recursive definition as theorems r10 7324, r1suc 7326, and r1lim 7328. Theorem r1val1 7342 shows a recursive definition that works for all values, and theorems r1val2 7393 and r1val3 7394 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 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  |-  R1  =  rec ( ( x  e. 
_V  |->  ~P x ) ,  (/) )

Detailed syntax breakdown of Definition df-r1
StepHypRef Expression
1 cr1 7318 . 2  class  R1
2 vx . . . 4  set  x
3 cvv 2727 . . . 4  class  _V
42cv 1618 . . . . 5  class  x
54cpw 3530 . . . 4  class  ~P x
62, 3, 5cmpt 3974 . . 3  class  ( x  e.  _V  |->  ~P x
)
7 c0 3362 . . 3  class  (/)
86, 7crdg 6308 . 2  class  rec (
( x  e.  _V  |->  ~P x ) ,  (/) )
91, 8wceq 1619 1  wff  R1  =  rec ( ( x  e. 
_V  |->  ~P x ) ,  (/) )
Colors of variables: wff set class
This definition is referenced by:  r1funlim  7322  r1fnon  7323  r10  7324  r1sucg  7325  r1limg  7327
  Copyright terms: Public domain W3C validator