Description: An ordinal number is equal to the union of its successor. (Contributed by NM, 12-Jun-1994)
Ref | Expression | ||
---|---|---|---|
Hypothesis | on.1 | |- A e. On |
|
Assertion | onunisuci | |- U. suc A = A |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | on.1 | |- A e. On |
|
2 | 1 | ontrci | |- Tr A |
3 | 1 | elexi | |- A e. _V |
4 | 3 | unisuc | |- ( Tr A <-> U. suc A = A ) |
5 | 2 4 | mpbi | |- U. suc A = A |