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	⊢ ( 𝐴 ∈ On → ( 𝑅1 ‘ suc 𝐴 ) = 𝒫 ( 𝑅1 ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		r1sucg	⊢ ( 𝐴 ∈ dom 𝑅1 → ( 𝑅1 ‘ suc 𝐴 ) = 𝒫 ( 𝑅1 ‘ 𝐴 ) )
2		r1fnon	⊢ 𝑅1 Fn On
3		fndm	⊢ ( 𝑅1 Fn On → dom 𝑅1 = On )
4	2 3	ax-mp	⊢ dom 𝑅1 = On
5	4	eqcomi	⊢ On = dom 𝑅1
6	1 5	eleq2s	⊢ ( 𝐴 ∈ On → ( 𝑅1 ‘ suc 𝐴 ) = 𝒫 ( 𝑅1 ‘ 𝐴 ) )