This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem brwdomi

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

		Ref	Expression
	Assertion	brwdomi	$⊢ X ≼^{*} Y \to (X = \emptyset \lor \exists z z : Y \underset{onto}{⟶} X)$

Step	Hyp	Ref	Expression
1		relwdom	$⊢ Rel ≼^{*}$
2	1	brrelex2i	$⊢ X ≼^{*} Y \to Y \in V$
3		brwdom	$⊢ Y \in V \to (X ≼^{*} Y \leftrightarrow (X = \emptyset \lor \exists z z : Y \underset{onto}{⟶} X))$
4	2 3	syl	$⊢ X ≼^{} Y \to (X ≼^{} Y \leftrightarrow (X = \emptyset \lor \exists z z : Y \underset{onto}{⟶} X))$
5	4	ibi	$⊢ X ≼^{*} Y \to (X = \emptyset \lor \exists z z : Y \underset{onto}{⟶} X)$