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