# 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 ${⊢}\left({A}\in \mathrm{dom}\mathrm{card}\wedge {B}\preccurlyeq {A}\right)\to {B}\in \mathrm{dom}\mathrm{card}$

### Proof

Step Hyp Ref Expression
1 cardon ${⊢}\mathrm{card}\left({A}\right)\in \mathrm{On}$
2 cardid2 ${⊢}{A}\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left({A}\right)\approx {A}$
3 domen2 ${⊢}\mathrm{card}\left({A}\right)\approx {A}\to \left({B}\preccurlyeq \mathrm{card}\left({A}\right)↔{B}\preccurlyeq {A}\right)$
4 2 3 syl ${⊢}{A}\in \mathrm{dom}\mathrm{card}\to \left({B}\preccurlyeq \mathrm{card}\left({A}\right)↔{B}\preccurlyeq {A}\right)$
5 4 biimpar ${⊢}\left({A}\in \mathrm{dom}\mathrm{card}\wedge {B}\preccurlyeq {A}\right)\to {B}\preccurlyeq \mathrm{card}\left({A}\right)$
6 ondomen ${⊢}\left(\mathrm{card}\left({A}\right)\in \mathrm{On}\wedge {B}\preccurlyeq \mathrm{card}\left({A}\right)\right)\to {B}\in \mathrm{dom}\mathrm{card}$
7 1 5 6 sylancr ${⊢}\left({A}\in \mathrm{dom}\mathrm{card}\wedge {B}\preccurlyeq {A}\right)\to {B}\in \mathrm{dom}\mathrm{card}$