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)\leftrightarrow B\preccurlyeq A\right)$$
4	2 3	syl	$$⊢A\in \mathrm{dom}\mathrm{card}\to \left(B\preccurlyeq \mathrm{card}\left(A\right)\leftrightarrow 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}$$