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 e. On -> ( ~P A i^i On ) = suc A )

Proof

Step Hyp Ref Expression
1 eloni
 |-  ( A e. On -> Ord A )
2 ordpwsuc
 |-  ( Ord A -> ( ~P A i^i On ) = suc A )
3 1 2 syl
 |-  ( A e. On -> ( ~P A i^i On ) = suc A )