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 ) )