Theorem dom2d

Description: A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. (Contributed by NM, 24-Jul-2004) (Revised by Mario Carneiro, 20-May-2013)

	Ref	Expression
Hypotheses	dom2d.1	$$⊢\phi \to \left(x\in A\to C\in B\right)$$
	dom2d.2	$$⊢\phi \to \left(\left(x\in A\wedge y\in A\right)\to \left(C=D\leftrightarrow x=y\right)\right)$$
Assertion	dom2d	$$⊢\phi \to \left(B\in R\to A\preccurlyeq B\right)$$

Proof

Step	Hyp	Ref	Expression
1		dom2d.1	$$⊢\phi \to \left(x\in A\to C\in B\right)$$
2		dom2d.2	$$⊢\phi \to \left(\left(x\in A\wedge y\in A\right)\to \left(C=D\leftrightarrow x=y\right)\right)$$
3	1 2	dom2lem	$$⊢\phi \to \left(x\in A⟼C\right):A\underset{1-1}{⟶}B$$
4		f1domg	$$⊢B\in R\to \left(\left(x\in A⟼C\right):A\underset{1-1}{⟶}B\to A\preccurlyeq B\right)$$
5	3 4	syl5com	$$⊢\phi \to \left(B\in R\to A\preccurlyeq B\right)$$