Theorem dom3d

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

	Ref	Expression
Hypotheses	dom2d.1	|- ( ph -> ( x e. A -> C e. B ) )
	dom2d.2	|- ( ph -> ( ( x e. A /\ y e. A ) -> ( C = D <-> x = y ) ) )
	dom3d.3	|- ( ph -> A e. V )
	dom3d.4	|- ( ph -> B e. W )
Assertion	dom3d	|- ( ph -> A ~<_ B )

Proof

Step	Hyp	Ref	Expression
1		dom2d.1	|- ( ph -> ( x e. A -> C e. B ) )
2		dom2d.2	|- ( ph -> ( ( x e. A /\ y e. A ) -> ( C = D <-> x = y ) ) )
3		dom3d.3	|- ( ph -> A e. V )
4		dom3d.4	|- ( ph -> B e. W )
5	1 2	dom2lem	|- ( ph -> ( x e. A |-> C ) : A -1-1-> B )
6		f1f	|- ( ( x e. A |-> C ) : A -1-1-> B -> ( x e. A |-> C ) : A --> B )
7	5 6	syl	|- ( ph -> ( x e. A |-> C ) : A --> B )
8		fex2	|- ( ( ( x e. A |-> C ) : A --> B /\ A e. V /\ B e. W ) -> ( x e. A |-> C ) e. _V )
9	7 3 4 8	syl3anc	|- ( ph -> ( x e. A |-> C ) e. _V )
10		f1eq1	|- ( z = ( x e. A |-> C ) -> ( z : A -1-1-> B <-> ( x e. A |-> C ) : A -1-1-> B ) )
11	9 5 10	spcedv	|- ( ph -> E. z z : A -1-1-> B )
12		brdomg	|- ( B e. W -> ( A ~<_ B <-> E. z z : A -1-1-> B ) )
13	4 12	syl	|- ( ph -> ( A ~<_ B <-> E. z z : A -1-1-> B ) )
14	11 13	mpbird	|- ( ph -> A ~<_ B )