Theorem brwdom3i

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

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

Proof

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