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 AVF:A1-1BFFinranFFin

Proof

Step Hyp Ref Expression
1 rnfi FFinranFFin
2 simpr AVF:A1-1BranFFinranFFin
3 f1dm F:A1-1BdomF=A
4 f1f1orn F:A1-1BF:A1-1 ontoranF
5 eleq1 A=domFAVdomFV
6 f1oeq2 A=domFF:A1-1 ontoranFF:domF1-1 ontoranF
7 5 6 anbi12d A=domFAVF:A1-1 ontoranFdomFVF:domF1-1 ontoranF
8 7 eqcoms domF=AAVF:A1-1 ontoranFdomFVF:domF1-1 ontoranF
9 8 biimpd domF=AAVF:A1-1 ontoranFdomFVF:domF1-1 ontoranF
10 9 expcomd domF=AF:A1-1 ontoranFAVdomFVF:domF1-1 ontoranF
11 3 4 10 sylc F:A1-1BAVdomFVF:domF1-1 ontoranF
12 11 impcom AVF:A1-1BdomFVF:domF1-1 ontoranF
13 12 adantr AVF:A1-1BranFFindomFVF:domF1-1 ontoranF
14 f1oeng domFVF:domF1-1 ontoranFdomFranF
15 13 14 syl AVF:A1-1BranFFindomFranF
16 enfii ranFFindomFranFdomFFin
17 2 15 16 syl2anc AVF:A1-1BranFFindomFFin
18 f1fun F:A1-1BFunF
19 18 ad2antlr AVF:A1-1BranFFinFunF
20 fundmfibi FunFFFindomFFin
21 19 20 syl AVF:A1-1BranFFinFFindomFFin
22 17 21 mpbird AVF:A1-1BranFFinFFin
23 22 ex AVF:A1-1BranFFinFFin
24 1 23 impbid2 AVF:A1-1BFFinranFFin