Metamath Proof Explorer

Theorem f1oexbi

Description: There is a one-to-one onto function from a set to a second set iff there is a one-to-one onto function from the second set to the first set. (Contributed by Alexander van der Vekens, 30-Sep-2018)

Ref Expression
Assertion f1oexbi ⊢ ∃ f f : A ⟶ 1-1 onto B ↔ ∃ g g : B ⟶ 1-1 onto A

Proof

Step Hyp Ref Expression
1 vex ⊢ f ∈ V
2 1 cnvex ⊢ f -1 ∈ V
3 f1ocnv ⊢ f : A ⟶ 1-1 onto B → f -1 : B ⟶ 1-1 onto A
4 f1oeq1 ⊢ g = f -1 → g : B ⟶ 1-1 onto A ↔ f -1 : B ⟶ 1-1 onto A
5 4 spcegv ⊢ f -1 ∈ V → f -1 : B ⟶ 1-1 onto A → ∃ g g : B ⟶ 1-1 onto A
6 2 3 5 mpsyl ⊢ f : A ⟶ 1-1 onto B → ∃ g g : B ⟶ 1-1 onto A
7 6 exlimiv ⊢ ∃ f f : A ⟶ 1-1 onto B → ∃ g g : B ⟶ 1-1 onto A
8 vex ⊢ g ∈ V
9 8 cnvex ⊢ g -1 ∈ V
10 f1ocnv ⊢ g : B ⟶ 1-1 onto A → g -1 : A ⟶ 1-1 onto B
11 f1oeq1 ⊢ f = g -1 → f : A ⟶ 1-1 onto B ↔ g -1 : A ⟶ 1-1 onto B
12 11 spcegv ⊢ g -1 ∈ V → g -1 : A ⟶ 1-1 onto B → ∃ f f : A ⟶ 1-1 onto B
13 9 10 12 mpsyl ⊢ g : B ⟶ 1-1 onto A → ∃ f f : A ⟶ 1-1 onto B
14 13 exlimiv ⊢ ∃ g g : B ⟶ 1-1 onto A → ∃ f f : A ⟶ 1-1 onto B
15 7 14 impbii ⊢ ∃ f f : A ⟶ 1-1 onto B ↔ ∃ g g : B ⟶ 1-1 onto A