Theorem brwdomi

Description: Property of weak dominance, forward direction only. (Contributed by Mario Carneiro, 5-May-2015)

	Ref	Expression
Assertion	brwdomi	$$⊢X{\preccurlyeq }^{*}Y\to \left(X=\varnothing \vee \exists zz:Y\underset{onto}{⟶}X\right)$$

Proof

Step	Hyp	Ref	Expression
1		relwdom	$$⊢\mathrm{Rel}{\preccurlyeq }^{*}$$
2	1	brrelex2i	$$⊢X{\preccurlyeq }^{*}Y\to Y\in \mathrm{V}$$
3		brwdom	$$⊢Y\in \mathrm{V}\to \left(X{\preccurlyeq }^{*}Y\leftrightarrow \left(X=\varnothing \vee \exists zz:Y\underset{onto}{⟶}X\right)\right)$$
4	2 3	syl	$$⊢X{\preccurlyeq }^{*}Y\to \left(X{\preccurlyeq }^{*}Y\leftrightarrow \left(X=\varnothing \vee \exists zz:Y\underset{onto}{⟶}X\right)\right)$$
5	4	ibi	$$⊢X{\preccurlyeq }^{*}Y\to \left(X=\varnothing \vee \exists zz:Y\underset{onto}{⟶}X\right)$$