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

Metamath Proof Explorer

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 )