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 | |
|
dom2d.2 | |
||
dom3d.3 | |
||
dom3d.4 | |
||
Assertion | dom3d | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dom2d.1 | |
|
2 | dom2d.2 | |
|
3 | dom3d.3 | |
|
4 | dom3d.4 | |
|
5 | 1 2 | dom2lem | |
6 | f1f | |
|
7 | 5 6 | syl | |
8 | fex2 | |
|
9 | 7 3 4 8 | syl3anc | |
10 | f1eq1 | |
|
11 | 9 5 10 | spcedv | |
12 | brdomg | |
|
13 | 4 12 | syl | |
14 | 11 13 | mpbird | |