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 ) |
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 ) |