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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elin | |
|
2 | velpw | |
|
3 | 2 | anbi2ci | |
4 | 1 3 | bitri | |
5 | ordsssuc | |
|
6 | 5 | expcom | |
7 | 6 | pm5.32d | |
8 | simpr | |
|
9 | ordsuc | |
|
10 | ordelon | |
|
11 | 10 | ex | |
12 | 9 11 | sylbi | |
13 | 12 | ancrd | |
14 | 8 13 | impbid2 | |
15 | 7 14 | bitrd | |
16 | 4 15 | bitrid | |
17 | 16 | eqrdv | |