Metamath Proof Explorer


Theorem numdom

Description: A set dominated by a numerable set is numerable. (Contributed by Mario Carneiro, 28-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 cardon
 |-  ( card ` A ) e. On
2 cardid2
 |-  ( A e. dom card -> ( card ` A ) ~~ A )
3 domen2
 |-  ( ( card ` A ) ~~ A -> ( B ~<_ ( card ` A ) <-> B ~<_ A ) )
4 2 3 syl
 |-  ( A e. dom card -> ( B ~<_ ( card ` A ) <-> B ~<_ A ) )
5 4 biimpar
 |-  ( ( A e. dom card /\ B ~<_ A ) -> B ~<_ ( card ` A ) )
6 ondomen
 |-  ( ( ( card ` A ) e. On /\ B ~<_ ( card ` A ) ) -> B e. dom card )
7 1 5 6 sylancr
 |-  ( ( A e. dom card /\ B ~<_ A ) -> B e. dom card )