This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 bitrid 
 |-  ( 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 )