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

Proof

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