Theorem wdomd

Description: Deduce weak dominance from an implicit onto function. (Contributed by Stefan O'Rear, 13-Feb-2015)

	Ref	Expression
Hypotheses	wdomd.b	|- ( ph -> B e. W )
	wdomd.o	|- ( ( ph /\ x e. A ) -> E. y e. B x = X )
Assertion	wdomd	|- ( ph -> A ~<_* B )

Proof

Step	Hyp	Ref	Expression
1		wdomd.b	|- ( ph -> B e. W )
2		wdomd.o	|- ( ( ph /\ x e. A ) -> E. y e. B x = X )
3		abrexexg	|- ( B e. W -> { x | E. y e. B x = X } e. _V )
4	1 3	syl	|- ( ph -> { x | E. y e. B x = X } e. _V )
5	2	ex	|- ( ph -> ( x e. A -> E. y e. B x = X ) )
6	5	alrimiv	|- ( ph -> A. x ( x e. A -> E. y e. B x = X ) )
7		ssab	|- ( A C_ { x | E. y e. B x = X } <-> A. x ( x e. A -> E. y e. B x = X ) )
8	6 7	sylibr	|- ( ph -> A C_ { x | E. y e. B x = X } )
9	4 8	ssexd	|- ( ph -> A e. _V )
10	9 1 2	wdom2d	|- ( ph -> A ~<_* B )