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

Metamath Proof Explorer

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 (F : A \underset{onto}{⟶} B \to B ≼ A)$

Proof

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