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 e. V /\ F : A -1-1-> B ) -> ( F e. Fin <-> ran F e. Fin ) )

Proof

Step Hyp Ref Expression
1 rnfi 
 |-  ( F e. Fin -> ran F e. Fin )
2 simpr 
 |-  ( ( ( A e. V /\ F : A -1-1-> B ) /\ ran F e. Fin ) -> ran F e. 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 e. V <-> dom F e. 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 e. V /\ F : A -1-1-onto-> ran F ) <-> ( dom F e. V /\ F : dom F -1-1-onto-> ran F ) ) )
8 7 eqcoms 
 |-  ( dom F = A -> ( ( A e. V /\ F : A -1-1-onto-> ran F ) <-> ( dom F e. V /\ F : dom F -1-1-onto-> ran F ) ) )
9 8 biimpd 
 |-  ( dom F = A -> ( ( A e. V /\ F : A -1-1-onto-> ran F ) -> ( dom F e. V /\ F : dom F -1-1-onto-> ran F ) ) )
10 9 expcomd 
 |-  ( dom F = A -> ( F : A -1-1-onto-> ran F -> ( A e. V -> ( dom F e. V /\ F : dom F -1-1-onto-> ran F ) ) ) )
11 3 4 10 sylc 
 |-  ( F : A -1-1-> B -> ( A e. V -> ( dom F e. V /\ F : dom F -1-1-onto-> ran F ) ) )
12 11 impcom 
 |-  ( ( A e. V /\ F : A -1-1-> B ) -> ( dom F e. V /\ F : dom F -1-1-onto-> ran F ) )
13 12 adantr 
 |-  ( ( ( A e. V /\ F : A -1-1-> B ) /\ ran F e. Fin ) -> ( dom F e. V /\ F : dom F -1-1-onto-> ran F ) )
14 f1oeng 
 |-  ( ( dom F e. V /\ F : dom F -1-1-onto-> ran F ) -> dom F ~~ ran F )
15 13 14 syl 
 |-  ( ( ( A e. V /\ F : A -1-1-> B ) /\ ran F e. Fin ) -> dom F ~~ ran F )
16 enfii 
 |-  ( ( ran F e. Fin /\ dom F ~~ ran F ) -> dom F e. Fin )
17 2 15 16 syl2anc 
 |-  ( ( ( A e. V /\ F : A -1-1-> B ) /\ ran F e. Fin ) -> dom F e. Fin )
18 f1fun 
 |-  ( F : A -1-1-> B -> Fun F )
19 18 ad2antlr 
 |-  ( ( ( A e. V /\ F : A -1-1-> B ) /\ ran F e. Fin ) -> Fun F )
20 fundmfibi 
 |-  ( Fun F -> ( F e. Fin <-> dom F e. Fin ) )
21 19 20 syl 
 |-  ( ( ( A e. V /\ F : A -1-1-> B ) /\ ran F e. Fin ) -> ( F e. Fin <-> dom F e. Fin ) )
22 17 21 mpbird 
 |-  ( ( ( A e. V /\ F : A -1-1-> B ) /\ ran F e. Fin ) -> F e. Fin )
23 22 ex 
 |-  ( ( A e. V /\ F : A -1-1-> B ) -> ( ran F e. Fin -> F e. Fin ) )
24 1 23 impbid2 
 |-  ( ( A e. V /\ F : A -1-1-> B ) -> ( F e. Fin <-> ran F e. Fin ) )