Metamath Proof Explorer


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 )