Metamath Proof Explorer


Theorem fodomnum

Description: A version of fodom that doesn't require the Axiom of Choice ax-ac . (Contributed by Mario Carneiro, 28-Feb-2013) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion fodomnum
|- ( A e. dom card -> ( F : A -onto-> B -> B ~<_ A ) )

Proof

Step Hyp Ref Expression
1 fornex
 |-  ( A e. dom card -> ( F : A -onto-> B -> B e. _V ) )
2 1 com12
 |-  ( F : A -onto-> B -> ( A e. dom card -> B e. _V ) )
3 numacn
 |-  ( B e. _V -> ( A e. dom card -> A e. AC_ B ) )
4 2 3 syli
 |-  ( F : A -onto-> B -> ( A e. dom card -> A e. AC_ B ) )
5 4 com12
 |-  ( A e. dom card -> ( F : A -onto-> B -> A e. AC_ B ) )
6 fodomacn
 |-  ( A e. AC_ B -> ( F : A -onto-> B -> B ~<_ A ) )
7 5 6 syli
 |-  ( A e. dom card -> ( F : A -onto-> B -> B ~<_ A ) )