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

Metamath Proof Explorer

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 )