Theorem f1oenfirn

Description: If the range of a one-to-one, onto function is finite, then the domain and range of the function are equinumerous. (Contributed by BTernaryTau, 9-Sep-2024)

	Ref	Expression
Assertion	f1oenfirn	|- ( ( B e. Fin /\ F : A -1-1-onto-> B ) -> A ~~ B )

Proof

Step	Hyp	Ref	Expression
1		f1ocnv	|- ( F : A -1-1-onto-> B -> `' F : B -1-1-onto-> A )
2		f1ofn	|- ( `' F : B -1-1-onto-> A -> `' F Fn B )
3		fnfi	|- ( ( `' F Fn B /\ B e. Fin ) -> `' F e. Fin )
4	2 3	sylan	|- ( ( `' F : B -1-1-onto-> A /\ B e. Fin ) -> `' F e. Fin )
5	1 4	sylan	|- ( ( F : A -1-1-onto-> B /\ B e. Fin ) -> `' F e. Fin )
6	5	ancoms	|- ( ( B e. Fin /\ F : A -1-1-onto-> B ) -> `' F e. Fin )
7		cnvfi	|- ( `' F e. Fin -> `' `' F e. Fin )
8		f1orel	|- ( F : A -1-1-onto-> B -> Rel F )
9		dfrel2	|- ( Rel F <-> `' `' F = F )
10	8 9	sylib	|- ( F : A -1-1-onto-> B -> `' `' F = F )
11	10	eleq1d	|- ( F : A -1-1-onto-> B -> ( `' `' F e. Fin <-> F e. Fin ) )
12	11	biimpac	|- ( ( `' `' F e. Fin /\ F : A -1-1-onto-> B ) -> F e. Fin )
13	7 12	sylan	|- ( ( `' F e. Fin /\ F : A -1-1-onto-> B ) -> F e. Fin )
14	6 13	sylancom	|- ( ( B e. Fin /\ F : A -1-1-onto-> B ) -> F e. Fin )
15		f1oen3g	|- ( ( F e. Fin /\ F : A -1-1-onto-> B ) -> A ~~ B )
16	14 15	sylancom	|- ( ( B e. Fin /\ F : A -1-1-onto-> B ) -> A ~~ B )