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 ) |
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 ) |