Theorem fodomg

Description: An onto function implies dominance of domain over range. Lemma 10.20 of Kunen p. 30. This theorem uses the axiom of choice ac7g . The axiom of choice is not needed for finite sets, see fodomfi . See also fodomnum . (Contributed by NM, 23-Jul-2004) (Proof shortened by BJ, 20-May-2024)

	Ref	Expression
Assertion	fodomg	$$⊢A\in V\to \left(F:A\underset{onto}{⟶}B\to B\preccurlyeq A\right)$$

Proof

Step	Hyp	Ref	Expression
1		numth3	$$⊢A\in V\to A\in \mathrm{dom}\mathrm{card}$$
2		fodomnum	$$⊢A\in \mathrm{dom}\mathrm{card}\to \left(F:A\underset{onto}{⟶}B\to B\preccurlyeq A\right)$$
3	1 2	syl	$$⊢A\in V\to \left(F:A\underset{onto}{⟶}B\to B\preccurlyeq A\right)$$