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 ) |