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 )