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 )