Theorem fodom

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

	Ref	Expression
Hypothesis	fodom.1	⊢ 𝐴 ∈ V
Assertion	fodom	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐵 ≼ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		fodom.1	⊢ 𝐴 ∈ V
2		fodomg	⊢ ( 𝐴 ∈ V → ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐵 ≼ 𝐴 ) )
3	1 2	ax-mp	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐵 ≼ 𝐴 )