Description: A one-to-one function whose domain is a set is finite if and only if its range is finite. See also f1vrnfibi . (Contributed by AV, 10-Jan-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | f1dmvrnfibi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rnfi | |
|
2 | simpr | |
|
3 | f1dm | |
|
4 | f1f1orn | |
|
5 | eleq1 | |
|
6 | f1oeq2 | |
|
7 | 5 6 | anbi12d | |
8 | 7 | eqcoms | |
9 | 8 | biimpd | |
10 | 9 | expcomd | |
11 | 3 4 10 | sylc | |
12 | 11 | impcom | |
13 | 12 | adantr | |
14 | f1oeng | |
|
15 | 13 14 | syl | |
16 | enfii | |
|
17 | 2 15 16 | syl2anc | |
18 | f1fun | |
|
19 | 18 | ad2antlr | |
20 | fundmfibi | |
|
21 | 19 20 | syl | |
22 | 17 21 | mpbird | |
23 | 22 | ex | |
24 | 1 23 | impbid2 | |