Metamath Proof Explorer


Theorem onsdom

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 )

Proof

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 )