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 ≼ Y \to X ≼^{*} Y$

Step	Hyp	Ref	Expression
1		neqne	$⊢ \neg X = \emptyset \to X \neq \emptyset$
2	1	adantl	$⊢ (X ≼ Y \land \neg X = \emptyset) \to X \neq \emptyset$
3		reldom	$⊢ Rel ≼$
4	3	brrelex1i	$⊢ X ≼ Y \to X \in V$
5		0sdomg	$⊢ X \in V \to (\emptyset ≺ X \leftrightarrow X \neq \emptyset)$
6	4 5	syl	$⊢ X ≼ Y \to (\emptyset ≺ X \leftrightarrow X \neq \emptyset)$
7	6	adantr	$⊢ (X ≼ Y \land \neg X = \emptyset) \to (\emptyset ≺ X \leftrightarrow X \neq \emptyset)$
8	2 7	mpbird	$⊢ (X ≼ Y \land \neg X = \emptyset) \to \emptyset ≺ X$
9		simpl	$⊢ (X ≼ Y \land \neg X = \emptyset) \to X ≼ Y$
10		fodomr	$⊢ (\emptyset ≺ X \land X ≼ Y) \to \exists y y : Y \underset{onto}{⟶} X$
11	8 9 10	syl2anc	$⊢ (X ≼ Y \land \neg X = \emptyset) \to \exists y y : Y \underset{onto}{⟶} X$
12	11	ex	$⊢ X ≼ Y \to (\neg X = \emptyset \to \exists y y : Y \underset{onto}{⟶} X)$
13	12	orrd	$⊢ X ≼ Y \to (X = \emptyset \lor \exists y y : Y \underset{onto}{⟶} X)$
14	3	brrelex2i	$⊢ X ≼ Y \to Y \in V$
15		brwdom	$⊢ Y \in V \to (X ≼^{*} Y \leftrightarrow (X = \emptyset \lor \exists y y : Y \underset{onto}{⟶} X))$
16	14 15	syl	$⊢ X ≼ Y \to (X ≼^{*} Y \leftrightarrow (X = \emptyset \lor \exists y y : Y \underset{onto}{⟶} X))$
17	13 16	mpbird	$⊢ X ≼ Y \to X ≼^{*} Y$

Metamath Proof Explorer