Description: Any well-orderable set is strictly dominated by an ordinal number. (Contributed by Jeff Hankins, 22-Oct-2009) (Proof shortened by Mario Carneiro, 15-May-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | onsdom | |- ( A e. dom card -> E. x e. On A ~< x ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | harcl | |- ( har ` A ) e. On |
|
| 2 | harsdom | |- ( A e. dom card -> A ~< ( har ` A ) ) |
|
| 3 | breq2 | |- ( x = ( har ` A ) -> ( A ~< x <-> A ~< ( har ` A ) ) ) |
|
| 4 | 3 | rspcev | |- ( ( ( har ` A ) e. On /\ A ~< ( har ` A ) ) -> E. x e. On A ~< x ) |
| 5 | 1 2 4 | sylancr | |- ( A e. dom card -> E. x e. On A ~< x ) |