This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )