Theorem domwdom

Description: Weak dominance is implied by dominance in the usual sense. (Contributed by Stefan O'Rear, 11-Feb-2015)

	Ref	Expression
Assertion	domwdom	$$⊢X\preccurlyeq Y\to X{\preccurlyeq }^{*}Y$$

Proof

Step	Hyp	Ref	Expression
1		neqne	$$⊢\neg X=\varnothing \to X\ne \varnothing$$
2	1	adantl	$$⊢\left(X\preccurlyeq Y\wedge \neg X=\varnothing \right)\to X\ne \varnothing$$
3		reldom	$$⊢\mathrm{Rel}\preccurlyeq$$
4	3	brrelex1i	$$⊢X\preccurlyeq Y\to X\in \mathrm{V}$$
5		0sdomg	$$⊢X\in \mathrm{V}\to \left(\varnothing \prec X\leftrightarrow X\ne \varnothing \right)$$
6	4 5	syl	$$⊢X\preccurlyeq Y\to \left(\varnothing \prec X\leftrightarrow X\ne \varnothing \right)$$
7	6	adantr	$$⊢\left(X\preccurlyeq Y\wedge \neg X=\varnothing \right)\to \left(\varnothing \prec X\leftrightarrow X\ne \varnothing \right)$$
8	2 7	mpbird	$$⊢\left(X\preccurlyeq Y\wedge \neg X=\varnothing \right)\to \varnothing \prec X$$
9		simpl	$$⊢\left(X\preccurlyeq Y\wedge \neg X=\varnothing \right)\to X\preccurlyeq Y$$
10		fodomr	$$⊢\left(\varnothing \prec X\wedge X\preccurlyeq Y\right)\to \exists yy:Y\underset{onto}{⟶}X$$
11	8 9 10	syl2anc	$$⊢\left(X\preccurlyeq Y\wedge \neg X=\varnothing \right)\to \exists yy:Y\underset{onto}{⟶}X$$
12	11	ex	$$⊢X\preccurlyeq Y\to \left(\neg X=\varnothing \to \exists yy:Y\underset{onto}{⟶}X\right)$$
13	12	orrd	$$⊢X\preccurlyeq Y\to \left(X=\varnothing \vee \exists yy:Y\underset{onto}{⟶}X\right)$$
14	3	brrelex2i	$$⊢X\preccurlyeq Y\to Y\in \mathrm{V}$$
15		brwdom	$$⊢Y\in \mathrm{V}\to \left(X{\preccurlyeq }^{*}Y\leftrightarrow \left(X=\varnothing \vee \exists yy:Y\underset{onto}{⟶}X\right)\right)$$
16	14 15	syl	$$⊢X\preccurlyeq Y\to \left(X{\preccurlyeq }^{*}Y\leftrightarrow \left(X=\varnothing \vee \exists yy:Y\underset{onto}{⟶}X\right)\right)$$
17	13 16	mpbird	$$⊢X\preccurlyeq Y\to X{\preccurlyeq }^{*}Y$$