Description: A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. (Contributed by NM, 24-Jul-2004) (Revised 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 ) ) ) |
||
| Assertion | dom2d | |- ( ph -> ( B e. R -> A ~<_ B ) ) |
| 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 | 1 2 | dom2lem | |- ( ph -> ( x e. A |-> C ) : A -1-1-> B ) |
| 4 | f1domg | |- ( B e. R -> ( ( x e. A |-> C ) : A -1-1-> B -> A ~<_ B ) ) |
|
| 5 | 3 4 | syl5com | |- ( ph -> ( B e. R -> A ~<_ B ) ) |