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

Metamath Proof Explorer

Theorem wdomnumr

Description: Weak dominance agrees with normal for numerable right sets. (Contributed by Stefan O'Rear, 28-Feb-2015) (Revised by Mario Carneiro, 5-May-2015)

Ref Expression
Assertion wdomnumr 
|- ( B e. dom card -> ( A ~<_* B <-> A ~<_ B ) )

Proof

Step Hyp Ref Expression
1 brwdom 
 |-  ( B e. dom card -> ( A ~<_* B <-> ( A = (/) \/ E. x x : B -onto-> A ) ) )
2 0domg 
 |-  ( B e. dom card -> (/) ~<_ B )
3 breq1 
 |-  ( A = (/) -> ( A ~<_ B <-> (/) ~<_ B ) )
4 2 3 syl5ibrcom 
 |-  ( B e. dom card -> ( A = (/) -> A ~<_ B ) )
5 fodomnum 
 |-  ( B e. dom card -> ( x : B -onto-> A -> A ~<_ B ) )
6 5 exlimdv 
 |-  ( B e. dom card -> ( E. x x : B -onto-> A -> A ~<_ B ) )
7 4 6 jaod 
 |-  ( B e. dom card -> ( ( A = (/) \/ E. x x : B -onto-> A ) -> A ~<_ B ) )
8 1 7 sylbid 
 |-  ( B e. dom card -> ( A ~<_* B -> A ~<_ B ) )
9 domwdom 
 |-  ( A ~<_ B -> A ~<_* B )
10 8 9 impbid1 
 |-  ( B e. dom card -> ( A ~<_* B <-> A ~<_ B ) )