This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 imbitrrid 
 |-  ( 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 ) )