Metamath Proof Explorer


Theorem onpwsuc

Description: The collection of ordinal numbers in the power set of an ordinal number is its successor. (Contributed by NM, 19-Oct-2004)

Ref Expression
Assertion onpwsuc A On 𝒫 A On = suc A

Proof

Step Hyp Ref Expression
1 eloni A On Ord A
2 ordpwsuc Ord A 𝒫 A On = suc A
3 1 2 syl A On 𝒫 A On = suc A