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

Metamath Proof Explorer

Theorem brwdom3i

Description: Weak dominance implies existence of a covering function. (Contributed by Stefan O'Rear, 13-Feb-2015)

		Ref	Expression
	Assertion	brwdom3i	$⊢ X ≼^{*} Y \to \exists f \forall x \in X \exists y \in Y x = f (y)$

Step	Hyp	Ref	Expression
1		relwdom	$⊢ Rel ≼^{*}$
2	1	brrelex1i	$⊢ X ≼^{*} Y \to X \in V$
3	1	brrelex2i	$⊢ X ≼^{*} Y \to Y \in V$
4		brwdom3	$⊢ (X \in V \land Y \in V) \to (X ≼^{*} Y \leftrightarrow \exists f \forall x \in X \exists y \in Y x = f (y))$
5	2 3 4	syl2anc	$⊢ X ≼^{} Y \to (X ≼^{} Y \leftrightarrow \exists f \forall x \in X \exists y \in Y x = f (y))$
6	5	ibi	$⊢ X ≼^{*} Y \to \exists f \forall x \in X \exists y \in Y x = f (y)$