Metamath Proof Explorer

Theorem fodom

Description: An onto function implies dominance of domain over range. (Contributed by NM, 23-Jul-2004)

Ref Expression
Hypothesis fodom.1 
|- A e. _V
Assertion fodom 
|- ( F : A -onto-> B -> B ~<_ A )

Proof

Step Hyp Ref Expression
1 fodom.1 
 |-  A e. _V
2 fodomg 
 |-  ( A e. _V -> ( F : A -onto-> B -> B ~<_ A ) )
3 1 2 ax-mp 
 |-  ( F : A -onto-> B -> B ~<_ A )