Theorem wdomac

Description: When assuming AC, weak and usual dominance coincide. It is not known if this is an AC equivalent. (Contributed by Stefan O'Rear, 11-Feb-2015) (Revised by Mario Carneiro, 5-May-2015)

	Ref	Expression
Assertion	wdomac	$$⊢X{\preccurlyeq }^{*}Y\leftrightarrow X\preccurlyeq Y$$

Proof

Step	Hyp	Ref	Expression
1		relwdom	$$⊢\mathrm{Rel}{\preccurlyeq }^{*}$$
2	1	brrelex2i	$$⊢X{\preccurlyeq }^{*}Y\to Y\in \mathrm{V}$$
3		reldom	$$⊢\mathrm{Rel}\preccurlyeq$$
4	3	brrelex2i	$$⊢X\preccurlyeq Y\to Y\in \mathrm{V}$$
5		numth3	$$⊢Y\in \mathrm{V}\to Y\in \mathrm{dom}\mathrm{card}$$
6		wdomnumr	$$⊢Y\in \mathrm{dom}\mathrm{card}\to \left(X{\preccurlyeq }^{*}Y\leftrightarrow X\preccurlyeq Y\right)$$
7	5 6	syl	$$⊢Y\in \mathrm{V}\to \left(X{\preccurlyeq }^{*}Y\leftrightarrow X\preccurlyeq Y\right)$$
8	2 4 7	pm5.21nii	$$⊢X{\preccurlyeq }^{*}Y\leftrightarrow X\preccurlyeq Y$$