Description: An ordinal number is either its own union (if zero or a limit ordinal) or the successor of its union. (Contributed by NM, 13-Jun-1994) Put in closed form. (Revised by BJ, 11-Jan-2025)
Ref | Expression | ||
---|---|---|---|
Assertion | onuniorsuc | |- ( A e. On -> ( A = U. A \/ A = suc U. A ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eloni | |- ( A e. On -> Ord A ) |
|
2 | orduniorsuc | |- ( Ord A -> ( A = U. A \/ A = suc U. A ) ) |
|
3 | 1 2 | syl | |- ( A e. On -> ( A = U. A \/ A = suc U. A ) ) |