Metamath Proof Explorer

Definition df-r1

Description: Define the cumulative hierarchy of sets function, using Takeuti and Zaring's notation ( R1 ). 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 ). Our definition expresses Definition 9.9 of TakeutiZaring p. 76 in a closed form, from which we derive the recursive definition as Theorems r10 , r1suc , and r1lim . Theorem r1val1 shows a recursive definition that works for all values, and Theorems r1val2 and r1val3 show the value expressed in terms of rank.

Other notations for this function areR 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)

		Ref	Expression
	Assertion	df-r1	$⊢ R_{1} = rec ((x \in V ⟼ 𝒫 x), \emptyset)$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cr1	$class R_{1}$
1		vx	$setvar x$
2		cvv	$class V$
3	1	cv	$setvar x$
4	3	cpw	$class 𝒫 x$
5	1 2 4	cmpt	$class (x \in V ⟼ 𝒫 x)$
6		c0	$class \emptyset$
7	5 6	crdg	$class rec ((x \in V ⟼ 𝒫 x), \emptyset)$
8	0 7	wceq	$wff R_{1} = rec ((x \in V ⟼ 𝒫 x), \emptyset)$