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

Proof

Step Hyp Ref Expression
1 elin
 |-  ( x e. ( ~P A i^i On ) <-> ( x e. ~P A /\ x e. On ) )
2 velpw
 |-  ( x e. ~P A <-> x C_ A )
3 2 anbi2ci
 |-  ( ( x e. ~P A /\ x e. On ) <-> ( x e. On /\ x C_ A ) )
4 1 3 bitri
 |-  ( x e. ( ~P A i^i On ) <-> ( x e. On /\ x C_ A ) )
5 ordsssuc
 |-  ( ( x e. On /\ Ord A ) -> ( x C_ A <-> x e. suc A ) )
6 5 expcom
 |-  ( Ord A -> ( x e. On -> ( x C_ A <-> x e. suc A ) ) )
7 6 pm5.32d
 |-  ( Ord A -> ( ( x e. On /\ x C_ A ) <-> ( x e. On /\ x e. suc A ) ) )
8 simpr
 |-  ( ( x e. On /\ x e. suc A ) -> x e. suc A )
9 ordsuc
 |-  ( Ord A <-> Ord suc A )
10 ordelon
 |-  ( ( Ord suc A /\ x e. suc A ) -> x e. On )
11 10 ex
 |-  ( Ord suc A -> ( x e. suc A -> x e. On ) )
12 9 11 sylbi
 |-  ( Ord A -> ( x e. suc A -> x e. On ) )
13 12 ancrd
 |-  ( Ord A -> ( x e. suc A -> ( x e. On /\ x e. suc A ) ) )
14 8 13 impbid2
 |-  ( Ord A -> ( ( x e. On /\ x e. suc A ) <-> x e. suc A ) )
15 7 14 bitrd
 |-  ( Ord A -> ( ( x e. On /\ x C_ A ) <-> x e. suc A ) )
16 4 15 syl5bb
 |-  ( Ord A -> ( x e. ( ~P A i^i On ) <-> x e. suc A ) )
17 16 eqrdv
 |-  ( Ord A -> ( ~P A i^i On ) = suc A )