This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem r1suc

Description: Value of the cumulative hierarchy of sets function at a successor ordinal. Part of Definition 9.9 of TakeutiZaring p. 76. (Contributed by NM, 2-Sep-2003) (Revised by Mario Carneiro, 10-Sep-2013)

		Ref	Expression
	Assertion	r1suc	$⊢ A \in On \to R_{1} (suc A) = 𝒫 R_{1} (A)$

Proof

Step	Hyp	Ref	Expression
1		r1sucg	$⊢ A \in dom R_{1} \to R_{1} (suc A) = 𝒫 R_{1} (A)$
2		r1fnon	$⊢ R_{1} Fn On$
3	2	fndmi	$⊢ dom R_{1} = On$
4	3	eqcomi	$⊢ On = dom R_{1}$
5	1 4	eleq2s	$⊢ A \in On \to R_{1} (suc A) = 𝒫 R_{1} (A)$