Theorem ondomen

Description: If a set is dominated by an ordinal, then it is numerable. (Contributed by Mario Carneiro, 5-Jan-2013)

	Ref	Expression
Assertion	ondomen	$$⊢\left(A\in \mathrm{On}\wedge B\preccurlyeq A\right)\to B\in \mathrm{dom}\mathrm{card}$$

Proof

Step	Hyp	Ref	Expression
1		breq2	$$⊢x=A\to \left(B\preccurlyeq x\leftrightarrow B\preccurlyeq A\right)$$
2	1	rspcev	$$⊢\left(A\in \mathrm{On}\wedge B\preccurlyeq A\right)\to \exists x\in \mathrm{On}B\preccurlyeq x$$
3		ac10ct	$$⊢\exists x\in \mathrm{On}B\preccurlyeq x\to \exists rr\mathrm{We}B$$
4	2 3	syl	$$⊢\left(A\in \mathrm{On}\wedge B\preccurlyeq A\right)\to \exists rr\mathrm{We}B$$
5		ween	$$⊢B\in \mathrm{dom}\mathrm{card}\leftrightarrow \exists rr\mathrm{We}B$$
6	4 5	sylibr	$$⊢\left(A\in \mathrm{On}\wedge B\preccurlyeq A\right)\to B\in \mathrm{dom}\mathrm{card}$$