Metamath Proof Explorer

Theorem fnrndomnum

Description: A version of fnrndomg that does not require the axiom of choice ax-ac . (Contributed by Vincent Gonzalez, 17-Aug-2026)

Ref Expression
Assertion fnrndomnum 
|- ( A e. dom card -> ( F Fn A -> ran F ~<_ A ) )

Proof

Step Hyp Ref Expression
1 dffn4 
 |-  ( F Fn A <-> F : A -onto-> ran F )
2 fodomnum 
 |-  ( A e. dom card -> ( F : A -onto-> ran F -> ran F ~<_ A ) )
3 1 2 biimtrid 
 |-  ( A e. dom card -> ( F Fn A -> ran F ~<_ A ) )