Metamath Proof Explorer

Theorem entrfil

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

Ref Expression
Assertion entrfil ⊢ A ∈ Fin ∧ A ≈ B ∧ B ≈ C → A ≈ C

Proof

Step Hyp Ref Expression
1 bren ⊢ B ≈ C ↔ ∃ f f : B ⟶ 1-1 onto C
2 bren ⊢ A ≈ B ↔ ∃ g g : A ⟶ 1-1 onto B
3 exdistrv ⊢ ∃ g ∃ f g : A ⟶ 1-1 onto B ∧ f : B ⟶ 1-1 onto C ↔ ∃ g g : A ⟶ 1-1 onto B ∧ ∃ f f : B ⟶ 1-1 onto C
4 19.42vv ⊢ ∃ g ∃ f A ∈ Fin ∧ g : A ⟶ 1-1 onto B ∧ f : B ⟶ 1-1 onto C ↔ A ∈ Fin ∧ ∃ g ∃ f g : A ⟶ 1-1 onto B ∧ f : B ⟶ 1-1 onto C
5 f1oco ⊢ f : B ⟶ 1-1 onto C ∧ g : A ⟶ 1-1 onto B → f ∘ g : A ⟶ 1-1 onto C
6 5 ancoms ⊢ g : A ⟶ 1-1 onto B ∧ f : B ⟶ 1-1 onto C → f ∘ g : A ⟶ 1-1 onto C
7 f1oenfi ⊢ A ∈ Fin ∧ f ∘ g : A ⟶ 1-1 onto C → A ≈ C
8 6 7 sylan2 ⊢ A ∈ Fin ∧ g : A ⟶ 1-1 onto B ∧ f : B ⟶ 1-1 onto C → A ≈ C
9 8 exlimivv ⊢ ∃ g ∃ f A ∈ Fin ∧ g : A ⟶ 1-1 onto B ∧ f : B ⟶ 1-1 onto C → A ≈ C
10 4 9 sylbir ⊢ A ∈ Fin ∧ ∃ g ∃ f g : A ⟶ 1-1 onto B ∧ f : B ⟶ 1-1 onto C → A ≈ C
11 3 10 sylan2br ⊢ A ∈ Fin ∧ ∃ g g : A ⟶ 1-1 onto B ∧ ∃ f f : B ⟶ 1-1 onto C → A ≈ C
12 11 3impb ⊢ A ∈ Fin ∧ ∃ g g : A ⟶ 1-1 onto B ∧ ∃ f f : B ⟶ 1-1 onto C → A ≈ C
13 2 12 syl3an2b ⊢ A ∈ Fin ∧ A ≈ B ∧ ∃ f f : B ⟶ 1-1 onto C → A ≈ C
14 1 13 syl3an3b ⊢ A ∈ Fin ∧ A ≈ B ∧ B ≈ C → A ≈ C