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 \in dom card \to (F Fn A \to ran F ≼ A)$

Step	Hyp	Ref	Expression
1		dffn4	$⊢ F Fn A \leftrightarrow F : A \underset{onto}{⟶} ran F$
2		fodomnum	$⊢ A \in dom card \to (F : A \underset{onto}{⟶} ran F \to ran F ≼ A)$
3	1 2	biimtrid	$⊢ A \in dom card \to (F Fn A \to ran F ≼ A)$