Theorem 0wdom

Description: Any set weakly dominates the empty set. (Contributed by Stefan O'Rear, 11-Feb-2015)

	Ref	Expression
Assertion	0wdom	$$⊢X\in V\to \varnothing {\preccurlyeq }^{*}X$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\varnothing =\varnothing$$
2	1	orci	$$⊢\left(\varnothing =\varnothing \vee \exists zz:X\underset{onto}{⟶}\varnothing \right)$$
3		brwdom	$$⊢X\in V\to \left(\varnothing {\preccurlyeq }^{*}X\leftrightarrow \left(\varnothing =\varnothing \vee \exists zz:X\underset{onto}{⟶}\varnothing \right)\right)$$
4	2 3	mpbiri	$$⊢X\in V\to \varnothing {\preccurlyeq }^{*}X$$