brwdomn0

Description: Weak dominance over nonempty sets. (Contributed by Stefan O'Rear, 11-Feb-2015) (Revised by Mario Carneiro, 5-May-2015)

		Ref	Expression
	Assertion	brwdomn0	$⊢ X \neq \emptyset \to (X ≼^{*} Y \leftrightarrow \exists z z : Y \underset{onto}{⟶} X)$

Step	Hyp	Ref	Expression
1		relwdom	$⊢ Rel ≼^{*}$
2	1	brrelex2i	$⊢ X ≼^{*} Y \to Y \in V$
3	2	a1i	$⊢ X \neq \emptyset \to (X ≼^{*} Y \to Y \in V)$
4		fof	$⊢ z : Y \underset{onto}{⟶} X \to z : Y ⟶ X$
5	4	fdmd	$⊢ z : Y \underset{onto}{⟶} X \to dom z = Y$
6		vex	$⊢ z \in V$
7	6	dmex	$⊢ dom z \in V$
8	5 7	eqeltrrdi	$⊢ z : Y \underset{onto}{⟶} X \to Y \in V$
9	8	exlimiv	$⊢ \exists z z : Y \underset{onto}{⟶} X \to Y \in V$
10	9	a1i	$⊢ X \neq \emptyset \to (\exists z z : Y \underset{onto}{⟶} X \to Y \in V)$
11		brwdom	$⊢ Y \in V \to (X ≼^{*} Y \leftrightarrow (X = \emptyset \lor \exists z z : Y \underset{onto}{⟶} X))$
12		df-ne	$⊢ X \neq \emptyset \leftrightarrow \neg X = \emptyset$
13		biorf	$⊢ \neg X = \emptyset \to (\exists z z : Y \underset{onto}{⟶} X \leftrightarrow (X = \emptyset \lor \exists z z : Y \underset{onto}{⟶} X))$
14	12 13	sylbi	$⊢ X \neq \emptyset \to (\exists z z : Y \underset{onto}{⟶} X \leftrightarrow (X = \emptyset \lor \exists z z : Y \underset{onto}{⟶} X))$
15	14	bicomd	$⊢ X \neq \emptyset \to ((X = \emptyset \lor \exists z z : Y \underset{onto}{⟶} X) \leftrightarrow \exists z z : Y \underset{onto}{⟶} X)$
16	11 15	sylan9bbr	$⊢ (X \neq \emptyset \land Y \in V) \to (X ≼^{*} Y \leftrightarrow \exists z z : Y \underset{onto}{⟶} X)$
17	16	ex	$⊢ X \neq \emptyset \to (Y \in V \to (X ≼^{*} Y \leftrightarrow \exists z z : Y \underset{onto}{⟶} X))$
18	3 10 17	pm5.21ndd	$⊢ X \neq \emptyset \to (X ≼^{*} Y \leftrightarrow \exists z z : Y \underset{onto}{⟶} X)$

Metamath Proof Explorer