Theorem wdomnumr

Description: Weak dominance agrees with normal for numerable right sets. (Contributed by Stefan O'Rear, 28-Feb-2015) (Revised by Mario Carneiro, 5-May-2015)

	Ref	Expression
Assertion	wdomnumr	$$⊢B\in \mathrm{dom}\mathrm{card}\to \left(A{\preccurlyeq }^{*}B\leftrightarrow A\preccurlyeq B\right)$$

Proof

Step	Hyp	Ref	Expression
1		brwdom	$$⊢B\in \mathrm{dom}\mathrm{card}\to \left(A{\preccurlyeq }^{*}B\leftrightarrow \left(A=\varnothing \vee \exists xx:B\underset{onto}{⟶}A\right)\right)$$
2		0domg	$$⊢B\in \mathrm{dom}\mathrm{card}\to \varnothing \preccurlyeq B$$
3		breq1	$$⊢A=\varnothing \to \left(A\preccurlyeq B\leftrightarrow \varnothing \preccurlyeq B\right)$$
4	2 3	syl5ibrcom	$$⊢B\in \mathrm{dom}\mathrm{card}\to \left(A=\varnothing \to A\preccurlyeq B\right)$$
5		fodomnum	$$⊢B\in \mathrm{dom}\mathrm{card}\to \left(x:B\underset{onto}{⟶}A\to A\preccurlyeq B\right)$$
6	5	exlimdv	$$⊢B\in \mathrm{dom}\mathrm{card}\to \left(\exists xx:B\underset{onto}{⟶}A\to A\preccurlyeq B\right)$$
7	4 6	jaod	$$⊢B\in \mathrm{dom}\mathrm{card}\to \left(\left(A=\varnothing \vee \exists xx:B\underset{onto}{⟶}A\right)\to A\preccurlyeq B\right)$$
8	1 7	sylbid	$$⊢B\in \mathrm{dom}\mathrm{card}\to \left(A{\preccurlyeq }^{*}B\to A\preccurlyeq B\right)$$
9		domwdom	$$⊢A\preccurlyeq B\to A{\preccurlyeq }^{*}B$$
10	8 9	impbid1	$$⊢B\in \mathrm{dom}\mathrm{card}\to \left(A{\preccurlyeq }^{*}B\leftrightarrow A\preccurlyeq B\right)$$