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 e. A -> C e. B )
	dom2.2	|- ( ( x e. A /\ y e. A ) -> ( C = D <-> x = y ) )
Assertion	dom3	|- ( ( A e. V /\ B e. W ) -> A ~<_ B )

Proof

Step	Hyp	Ref	Expression
1		dom2.1	|- ( x e. A -> C e. B )
2		dom2.2	|- ( ( x e. A /\ y e. A ) -> ( C = D <-> x = y ) )
3	1	a1i	|- ( ( A e. V /\ B e. W ) -> ( x e. A -> C e. B ) )
4	2	a1i	|- ( ( A e. V /\ B e. W ) -> ( ( x e. A /\ y e. A ) -> ( C = D <-> x = y ) ) )
5		simpl	|- ( ( A e. V /\ B e. W ) -> A e. V )
6		simpr	|- ( ( A e. V /\ B e. W ) -> B e. W )
7	3 4 5 6	dom3d	|- ( ( A e. V /\ B e. W ) -> A ~<_ B )