Metamath Proof Explorer


Theorem f1vrnfibi

Description: A one-to-one function which is a set is finite if and only if its range is finite. See also f1dmvrnfibi . (Contributed by AV, 10-Jan-2020)

Ref Expression
Assertion f1vrnfibi
|- ( ( F e. V /\ F : A -1-1-> B ) -> ( F e. Fin <-> ran F e. Fin ) )

Proof

Step Hyp Ref Expression
1 f1dm
 |-  ( F : A -1-1-> B -> dom F = A )
2 dmexg
 |-  ( F e. V -> dom F e. _V )
3 eleq1
 |-  ( A = dom F -> ( A e. _V <-> dom F e. _V ) )
4 3 eqcoms
 |-  ( dom F = A -> ( A e. _V <-> dom F e. _V ) )
5 2 4 syl5ibr
 |-  ( dom F = A -> ( F e. V -> A e. _V ) )
6 1 5 syl
 |-  ( F : A -1-1-> B -> ( F e. V -> A e. _V ) )
7 6 impcom
 |-  ( ( F e. V /\ F : A -1-1-> B ) -> A e. _V )
8 f1dmvrnfibi
 |-  ( ( A e. _V /\ F : A -1-1-> B ) -> ( F e. Fin <-> ran F e. Fin ) )
9 7 8 sylancom
 |-  ( ( F e. V /\ F : A -1-1-> B ) -> ( F e. Fin <-> ran F e. Fin ) )