Metamath Proof Explorer

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 \in Fin \land A \approx B \land B \approx C) \to A \approx C$

Proof

Step	Hyp	Ref	Expression
1		enfii	$⊢ (B \in Fin \land A \approx B) \to A \in Fin$
2	1	3adant3	$⊢ (B \in Fin \land A \approx B \land B \approx C) \to A \in Fin$
3		entrfil	$⊢ (A \in Fin \land A \approx B \land B \approx C) \to A \approx C$
4	2 3	syld3an1	$⊢ (B \in Fin \land A \approx B \land B \approx C) \to A \approx C$