Metamath Proof Explorer

Theorem entrfir

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

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

Proof

Step Hyp Ref Expression
1 enfii ⊢ C ∈ Fin ∧ B ≈ C → B ∈ Fin
2 1 3adant2 ⊢ C ∈ Fin ∧ A ≈ B ∧ B ≈ C → B ∈ Fin
3 entrfi ⊢ B ∈ Fin ∧ A ≈ B ∧ B ≈ C → A ≈ C
4 2 3 syld3an1 ⊢ C ∈ Fin ∧ A ≈ B ∧ B ≈ C → A ≈ C