Theorem entrfi

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	entrfi	|- ( ( B e. Fin /\ A ~~ B /\ B ~~ C ) -> A ~~ C )

Proof

Step	Hyp	Ref	Expression
1		enfii	|- ( ( B e. Fin /\ A ~~ B ) -> A e. Fin )
2	1	3adant3	|- ( ( B e. Fin /\ A ~~ B /\ B ~~ C ) -> A e. Fin )
3		entrfil	|- ( ( A e. Fin /\ A ~~ B /\ B ~~ C ) -> A ~~ C )
4	2 3	syld3an1	|- ( ( B e. Fin /\ A ~~ B /\ B ~~ C ) -> A ~~ C )