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 ∈ Fin ∧ F : A ⟶ 1-1 onto B → A ≈ B

Proof

Step Hyp Ref Expression
1 f1ocnv ⊢ F : A ⟶ 1-1 onto B → F -1 : B ⟶ 1-1 onto A
2 f1ofn ⊢ F -1 : B ⟶ 1-1 onto A → F -1 Fn B
3 fnfi ⊢ F -1 Fn B ∧ B ∈ Fin → F -1 ∈ Fin
4 2 3 sylan ⊢ F -1 : B ⟶ 1-1 onto A ∧ B ∈ Fin → F -1 ∈ Fin
5 1 4 sylan ⊢ F : A ⟶ 1-1 onto B ∧ B ∈ Fin → F -1 ∈ Fin
6 5 ancoms ⊢ B ∈ Fin ∧ F : A ⟶ 1-1 onto B → F -1 ∈ Fin
7 cnvfi ⊢ F -1 ∈ Fin → F -1 -1 ∈ Fin
8 f1orel ⊢ F : A ⟶ 1-1 onto B → Rel ⁡ F
9 dfrel2 ⊢ Rel ⁡ F ↔ F -1 -1 = F
10 8 9 sylib ⊢ F : A ⟶ 1-1 onto B → F -1 -1 = F
11 10 eleq1d ⊢ F : A ⟶ 1-1 onto B → F -1 -1 ∈ Fin ↔ F ∈ Fin
12 11 biimpac ⊢ F -1 -1 ∈ Fin ∧ F : A ⟶ 1-1 onto B → F ∈ Fin
13 7 12 sylan ⊢ F -1 ∈ Fin ∧ F : A ⟶ 1-1 onto B → F ∈ Fin
14 6 13 sylancom ⊢ B ∈ Fin ∧ F : A ⟶ 1-1 onto B → F ∈ Fin
15 f1oen3g ⊢ F ∈ Fin ∧ F : A ⟶ 1-1 onto B → A ≈ B
16 14 15 sylancom ⊢ B ∈ Fin ∧ F : A ⟶ 1-1 onto B → A ≈ B