Metamath Proof Explorer

Theorem fonum

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

Ref Expression
Assertion fonum 
|- ( ( A e. dom card /\ F : A -onto-> B ) -> B e. dom card )

Proof

Step Hyp Ref Expression
1 fodomnum 
 |-  ( A e. dom card -> ( F : A -onto-> B -> B ~<_ A ) )
2 1 imp 
 |-  ( ( A e. dom card /\ F : A -onto-> B ) -> B ~<_ A )
3 numdom 
 |-  ( ( A e. dom card /\ B ~<_ A ) -> B e. dom card )
4 2 3 syldan 
 |-  ( ( A e. dom card /\ F : A -onto-> B ) -> B e. dom card )