fowdom

Description: An onto function implies weak dominance. (Contributed by Stefan O'Rear, 11-Feb-2015)

		Ref	Expression
	Assertion	fowdom	$⊢ (F \in V \land F : Y \underset{onto}{⟶} X) \to X ≼^{*} Y$

Step	Hyp	Ref	Expression
1		elex	$⊢ F \in V \to F \in V$
2		foeq1	$⊢ z = F \to (z : Y \underset{onto}{⟶} X \leftrightarrow F : Y \underset{onto}{⟶} X)$
3	2	spcegv	$⊢ F \in V \to (F : Y \underset{onto}{⟶} X \to \exists z z : Y \underset{onto}{⟶} X)$
4	3	imp	$⊢ (F \in V \land F : Y \underset{onto}{⟶} X) \to \exists z z : Y \underset{onto}{⟶} X$
5	4	olcd	$⊢ (F \in V \land F : Y \underset{onto}{⟶} X) \to (X = \emptyset \lor \exists z z : Y \underset{onto}{⟶} X)$
6		fof	$⊢ F : Y \underset{onto}{⟶} X \to F : Y ⟶ X$
7		dmfex	$⊢ (F \in V \land F : Y ⟶ X) \to Y \in V$
8	6 7	sylan2	$⊢ (F \in V \land F : Y \underset{onto}{⟶} X) \to Y \in V$
9		brwdom	$⊢ Y \in V \to (X ≼^{*} Y \leftrightarrow (X = \emptyset \lor \exists z z : Y \underset{onto}{⟶} X))$
10	8 9	syl	$⊢ (F \in V \land F : Y \underset{onto}{⟶} X) \to (X ≼^{*} Y \leftrightarrow (X = \emptyset \lor \exists z z : Y \underset{onto}{⟶} X))$
11	5 10	mpbird	$⊢ (F \in V \land F : Y \underset{onto}{⟶} X) \to X ≼^{*} Y$
12	1 11	sylan	$⊢ (F \in V \land F : Y \underset{onto}{⟶} X) \to X ≼^{*} Y$

Metamath Proof Explorer