Metamath Proof Explorer

Theorem isnumi

Description: A set equinumerous to an ordinal is numerable. (Contributed by Mario Carneiro, 29-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( x = A -> ( x ~~ B <-> A ~~ B ) )
2 1 rspcev 
 |-  ( ( A e. On /\ A ~~ B ) -> E. x e. On x ~~ B )
3 isnum2 
 |-  ( B e. dom card <-> E. x e. On x ~~ B )
4 2 3 sylibr 
 |-  ( ( A e. On /\ A ~~ B ) -> B e. dom card )