Theorem dom3

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 Mario Carneiro, 20-May-2013)

	Ref	Expression
Hypotheses	dom2.1	$$⊢x\in A\to C\in B$$
	dom2.2	$$⊢\left(x\in A\wedge y\in A\right)\to \left(C=D\leftrightarrow x=y\right)$$
Assertion	dom3	$$⊢\left(A\in V\wedge B\in W\right)\to A\preccurlyeq B$$

Proof

Step	Hyp	Ref	Expression
1		dom2.1	$$⊢x\in A\to C\in B$$
2		dom2.2	$$⊢\left(x\in A\wedge y\in A\right)\to \left(C=D\leftrightarrow x=y\right)$$
3	1	a1i	$$⊢\left(A\in V\wedge B\in W\right)\to \left(x\in A\to C\in B\right)$$
4	2	a1i	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\left(x\in A\wedge y\in A\right)\to \left(C=D\leftrightarrow x=y\right)\right)$$
5		simpl	$$⊢\left(A\in V\wedge B\in W\right)\to A\in V$$
6		simpr	$$⊢\left(A\in V\wedge B\in W\right)\to B\in W$$
7	3 4 5 6	dom3d	$$⊢\left(A\in V\wedge B\in W\right)\to A\preccurlyeq B$$