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 0fin
 |-  (/) 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 )