Metamath Proof Explorer

Theorem ensymfib

Description: Symmetry of equinumerosity for finite sets, proved without using the Axiom of Power Sets (unlike ensymb ). (Contributed by BTernaryTau, 9-Sep-2024)

Ref Expression
Assertion ensymfib ⊢ A ∈ Fin → A ≈ B ↔ B ≈ A

Proof

Step Hyp Ref Expression
1 bren ⊢ A ≈ B ↔ ∃ f f : A ⟶ 1-1 onto B
2 19.42v ⊢ ∃ f A ∈ Fin ∧ f : A ⟶ 1-1 onto B ↔ A ∈ Fin ∧ ∃ f f : A ⟶ 1-1 onto B
3 f1ocnv ⊢ f : A ⟶ 1-1 onto B → f -1 : B ⟶ 1-1 onto A
4 f1oenfirn ⊢ A ∈ Fin ∧ f -1 : B ⟶ 1-1 onto A → B ≈ A
5 3 4 sylan2 ⊢ A ∈ Fin ∧ f : A ⟶ 1-1 onto B → B ≈ A
6 5 exlimiv ⊢ ∃ f A ∈ Fin ∧ f : A ⟶ 1-1 onto B → B ≈ A
7 2 6 sylbir ⊢ A ∈ Fin ∧ ∃ f f : A ⟶ 1-1 onto B → B ≈ A
8 1 7 sylan2b ⊢ A ∈ Fin ∧ A ≈ B → B ≈ A
9 bren ⊢ B ≈ A ↔ ∃ g g : B ⟶ 1-1 onto A
10 19.42v ⊢ ∃ g A ∈ Fin ∧ g : B ⟶ 1-1 onto A ↔ A ∈ Fin ∧ ∃ g g : B ⟶ 1-1 onto A
11 f1ocnv ⊢ g : B ⟶ 1-1 onto A → g -1 : A ⟶ 1-1 onto B
12 f1oenfi ⊢ A ∈ Fin ∧ g -1 : A ⟶ 1-1 onto B → A ≈ B
13 11 12 sylan2 ⊢ A ∈ Fin ∧ g : B ⟶ 1-1 onto A → A ≈ B
14 13 exlimiv ⊢ ∃ g A ∈ Fin ∧ g : B ⟶ 1-1 onto A → A ≈ B
15 10 14 sylbir ⊢ A ∈ Fin ∧ ∃ g g : B ⟶ 1-1 onto A → A ≈ B
16 9 15 sylan2b ⊢ A ∈ Fin ∧ B ≈ A → A ≈ B
17 8 16 impbida ⊢ A ∈ Fin → A ≈ B ↔ B ≈ A