Metamath Proof Explorer


Theorem ordpwsuc

Description: The collection of ordinals in the power class of an ordinal is its successor. (Contributed by NM, 30-Jan-2005)

Ref Expression
Assertion ordpwsuc OrdA𝒫AOn=sucA

Proof

Step Hyp Ref Expression
1 elin x𝒫AOnx𝒫AxOn
2 velpw x𝒫AxA
3 2 anbi2ci x𝒫AxOnxOnxA
4 1 3 bitri x𝒫AOnxOnxA
5 ordsssuc xOnOrdAxAxsucA
6 5 expcom OrdAxOnxAxsucA
7 6 pm5.32d OrdAxOnxAxOnxsucA
8 simpr xOnxsucAxsucA
9 ordsuc OrdAOrdsucA
10 ordelon OrdsucAxsucAxOn
11 10 ex OrdsucAxsucAxOn
12 9 11 sylbi OrdAxsucAxOn
13 12 ancrd OrdAxsucAxOnxsucA
14 8 13 impbid2 OrdAxOnxsucAxsucA
15 7 14 bitrd OrdAxOnxAxsucA
16 4 15 bitrid OrdAx𝒫AOnxsucA
17 16 eqrdv OrdA𝒫AOn=sucA