Metamath Proof Explorer

Theorem numwdom

Description: A surjection maps numerable sets to numerable sets. (Contributed by Mario Carneiro, 27-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 brwdomi 
 |-  ( B ~<_* A -> ( B = (/) \/ E. f f : A -onto-> B ) )
2 simpr 
 |-  ( ( A e. dom card /\ B = (/) ) -> B = (/) )
3 0fi 
 |-  (/) e. Fin
4 finnum 
 |-  ( (/) e. Fin -> (/) e. dom card )
5 3 4 ax-mp 
 |-  (/) e. dom card
6 2 5 eqeltrdi 
 |-  ( ( A e. dom card /\ B = (/) ) -> B e. dom card )
7 fonum 
 |-  ( ( A e. dom card /\ f : A -onto-> B ) -> B e. dom card )
8 7 ex 
 |-  ( A e. dom card -> ( f : A -onto-> B -> B e. dom card ) )
9 8 exlimdv 
 |-  ( A e. dom card -> ( E. f f : A -onto-> B -> B e. dom card ) )
10 9 imp 
 |-  ( ( A e. dom card /\ E. f f : A -onto-> B ) -> B e. dom card )
11 6 10 jaodan 
 |-  ( ( A e. dom card /\ ( B = (/) \/ E. f f : A -onto-> B ) ) -> B e. dom card )
12 1 11 sylan2 
 |-  ( ( A e. dom card /\ B ~<_* A ) -> B e. dom card )