Metamath Proof Explorer


Theorem ondomen

Description: If a set is dominated by an ordinal, then it is numerable. (Contributed by Mario Carneiro, 5-Jan-2013)

Ref Expression
Assertion ondomen
|- ( ( A e. On /\ B ~<_ A ) -> B e. dom card )

Proof

Step Hyp Ref Expression
1 breq2
 |-  ( x = A -> ( B ~<_ x <-> B ~<_ A ) )
2 1 rspcev
 |-  ( ( A e. On /\ B ~<_ A ) -> E. x e. On B ~<_ x )
3 ac10ct
 |-  ( E. x e. On B ~<_ x -> E. r r We B )
4 2 3 syl
 |-  ( ( A e. On /\ B ~<_ A ) -> E. r r We B )
5 ween
 |-  ( B e. dom card <-> E. r r We B )
6 4 5 sylibr
 |-  ( ( A e. On /\ B ~<_ A ) -> B e. dom card )