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

Metamath Proof Explorer

Theorem dom2

Description: A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. C and D can be read C ( x ) and D ( y ) , as can be inferred from their distinct variable conditions. (Contributed by NM, 26-Oct-2003)

	Ref	Expression
Hypotheses	dom2.1	$⊢ x \in A \to C \in B$
	dom2.2	$⊢ (x \in A \land y \in A) \to (C = D \leftrightarrow x = y)$
Assertion	dom2	$⊢ B \in V \to A ≼ B$

Proof

Step	Hyp	Ref	Expression
1		dom2.1	$⊢ x \in A \to C \in B$
2		dom2.2	$⊢ (x \in A \land y \in A) \to (C = D \leftrightarrow x = y)$
3		eqid	$⊢ A = A$
4	1	a1i	$⊢ A = A \to (x \in A \to C \in B)$
5	2	a1i	$⊢ A = A \to ((x \in A \land y \in A) \to (C = D \leftrightarrow x = y))$
6	4 5	dom2d	$⊢ A = A \to (B \in V \to A ≼ B)$
7	3 6	ax-mp	$⊢ B \in V \to A ≼ B$