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 -> E. f A. x e. X E. y e. Y x = ( f ` y ) )

Proof

Step	Hyp	Ref	Expression
1		relwdom	|- Rel ~<_*
2	1	brrelex1i	|- ( X ~<_* Y -> X e. _V )
3	1	brrelex2i	|- ( X ~<_* Y -> Y e. _V )
4		brwdom3	|- ( ( X e. _V /\ Y e. _V ) -> ( X ~<_* Y <-> E. f A. x e. X E. y e. Y x = ( f ` y ) ) )
5	2 3 4	syl2anc	|- ( X ~<_* Y -> ( X ~<_* Y <-> E. f A. x e. X E. y e. Y x = ( f ` y ) ) )
6	5	ibi	|- ( X ~<_* Y -> E. f A. x e. X E. y e. Y x = ( f ` y ) )