This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in V$
	Assertion	fodom	$⊢ F : A \underset{onto}{⟶} B \to B ≼ A$

Step	Hyp	Ref	Expression
1		fodom.1	$⊢ A \in V$
2		fodomg	$⊢ A \in V \to (F : A \underset{onto}{⟶} B \to B ≼ A)$
3	1 2	ax-mp	$⊢ F : A \underset{onto}{⟶} B \to B ≼ A$