Metamath Proof Explorer


Theorem f1dmvrnfibi

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 A V F : A 1-1 B F Fin ran F Fin

Proof

Step Hyp Ref Expression
1 rnfi F Fin ran F Fin
2 simpr A V F : A 1-1 B ran F Fin ran F Fin
3 f1dm F : A 1-1 B dom F = A
4 f1f1orn F : A 1-1 B F : A 1-1 onto ran F
5 eleq1 A = dom F A V dom F V
6 f1oeq2 A = dom F F : A 1-1 onto ran F F : dom F 1-1 onto ran F
7 5 6 anbi12d A = dom F A V F : A 1-1 onto ran F dom F V F : dom F 1-1 onto ran F
8 7 eqcoms dom F = A A V F : A 1-1 onto ran F dom F V F : dom F 1-1 onto ran F
9 8 biimpd dom F = A A V F : A 1-1 onto ran F dom F V F : dom F 1-1 onto ran F
10 9 expcomd dom F = A F : A 1-1 onto ran F A V dom F V F : dom F 1-1 onto ran F
11 3 4 10 sylc F : A 1-1 B A V dom F V F : dom F 1-1 onto ran F
12 11 impcom A V F : A 1-1 B dom F V F : dom F 1-1 onto ran F
13 12 adantr A V F : A 1-1 B ran F Fin dom F V F : dom F 1-1 onto ran F
14 f1oeng dom F V F : dom F 1-1 onto ran F dom F ran F
15 13 14 syl A V F : A 1-1 B ran F Fin dom F ran F
16 enfii ran F Fin dom F ran F dom F Fin
17 2 15 16 syl2anc A V F : A 1-1 B ran F Fin dom F Fin
18 f1fun F : A 1-1 B Fun F
19 18 ad2antlr A V F : A 1-1 B ran F Fin Fun F
20 fundmfibi Fun F F Fin dom F Fin
21 19 20 syl A V F : A 1-1 B ran F Fin F Fin dom F Fin
22 17 21 mpbird A V F : A 1-1 B ran F Fin F Fin
23 22 ex A V F : A 1-1 B ran F Fin F Fin
24 1 23 impbid2 A V F : A 1-1 B F Fin ran F Fin