Description: The union of a set of ordinal numbers is an ordinal number. Corollary 7N(d) of Enderton p. 193. (Contributed by NM, 20-Sep-2003)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ssonuni.1 | |- A e. _V |
|
Assertion | ssonunii | |- ( A C_ On -> U. A e. On ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssonuni.1 | |- A e. _V |
|
2 | ssonuni | |- ( A e. _V -> ( A C_ On -> U. A e. On ) ) |
|
3 | 1 2 | ax-mp | |- ( A C_ On -> U. A e. On ) |