Description: Membership of the class of successor ordinals. (Contributed by Chen-Pang He, 1-Nov-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ordtoplem.1 | |
|
Assertion | ordtoplem | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ordtoplem.1 | |
|
2 | df-ne | |
|
3 | ordeleqon | |
|
4 | unon | |
|
5 | 4 | eqcomi | |
6 | id | |
|
7 | unieq | |
|
8 | 5 6 7 | 3eqtr4a | |
9 | 8 | orim2i | |
10 | 3 9 | sylbi | |
11 | 10 | orcomd | |
12 | 11 | ord | |
13 | orduniorsuc | |
|
14 | 13 | ord | |
15 | onuni | |
|
16 | eleq1a | |
|
17 | 15 1 16 | 3syl | |
18 | 12 14 17 | syl6c | |
19 | 2 18 | biimtrid | |