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 )