Metamath Proof Explorer


Theorem dom2

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 NM, 26-Oct-2003)

Ref Expression
Hypotheses dom2.1
|- ( x e. A -> C e. B )
dom2.2
|- ( ( x e. A /\ y e. A ) -> ( C = D <-> x = y ) )
Assertion dom2
|- ( B e. V -> 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 eqid
 |-  A = A
4 1 a1i
 |-  ( A = A -> ( x e. A -> C e. B ) )
5 2 a1i
 |-  ( A = A -> ( ( x e. A /\ y e. A ) -> ( C = D <-> x = y ) ) )
6 4 5 dom2d
 |-  ( A = A -> ( B e. V -> A ~<_ B ) )
7 3 6 ax-mp
 |-  ( B e. V -> A ~<_ B )