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)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dom2d.1 | |
|
dom2d.2 | |
||
Assertion | dom2lem | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dom2d.1 | |
|
2 | dom2d.2 | |
|
3 | 1 | ralrimiv | |
4 | eqid | |
|
5 | 4 | fmpt | |
6 | 3 5 | sylib | |
7 | 1 | imp | |
8 | 4 | fvmpt2 | |
9 | 8 | adantll | |
10 | 7 9 | mpdan | |
11 | 10 | adantrr | |
12 | nfv | |
|
13 | nffvmpt1 | |
|
14 | 13 | nfeq1 | |
15 | 12 14 | nfim | |
16 | eleq1w | |
|
17 | 16 | anbi2d | |
18 | 17 | imbi1d | |
19 | 16 | anbi1d | |
20 | anidm | |
|
21 | 19 20 | bitrdi | |
22 | 21 | anbi2d | |
23 | fveq2 | |
|
24 | 23 | adantr | |
25 | 2 | imp | |
26 | 25 | biimparc | |
27 | 24 26 | eqeq12d | |
28 | 27 | ex | |
29 | 22 28 | sylbird | |
30 | 29 | pm5.74d | |
31 | 18 30 | bitrd | |
32 | 15 31 10 | chvarfv | |
33 | 32 | adantrl | |
34 | 11 33 | eqeq12d | |
35 | 25 | biimpd | |
36 | 34 35 | sylbid | |
37 | 36 | ralrimivva | |
38 | nfmpt1 | |
|
39 | nfcv | |
|
40 | 38 39 | dff13f | |
41 | 6 37 40 | sylanbrc | |