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

Proof

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