Description: A is called a successor ordinal if it is not a limit ordinal and not the empty set. (Contributed by RP, 11-Nov-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | dfsucon | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3ancomb | |
|
2 | df-3an | |
|
3 | df-ne | |
|
4 | 3 | anbi2i | |
5 | 4 | imbi1i | |
6 | pm5.6 | |
|
7 | iman | |
|
8 | 5 6 7 | 3bitrri | |
9 | dflim3 | |
|
10 | 8 9 | xchnxbir | |
11 | 10 | anbi2i | |
12 | 1 2 11 | 3bitri | |
13 | pm3.35 | |
|
14 | 12 13 | sylbi | |
15 | eloni | |
|
16 | ordsuc | |
|
17 | 15 16 | sylib | |
18 | nlimsucg | |
|
19 | nsuceq0 | |
|
20 | 19 | a1i | |
21 | 17 18 20 | 3jca | |
22 | ordeq | |
|
23 | limeq | |
|
24 | 23 | notbid | |
25 | neeq1 | |
|
26 | 22 24 25 | 3anbi123d | |
27 | 21 26 | syl5ibrcom | |
28 | 27 | rexlimiv | |
29 | 14 28 | impbii | |