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	⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶 ) → 𝐴 ≈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		enfii	⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ≈ 𝐵 ) → 𝐴 ∈ Fin )
2	1	3adant3	⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶 ) → 𝐴 ∈ Fin )
3		entrfil	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶 ) → 𝐴 ≈ 𝐶 )
4	2 3	syld3an1	⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶 ) → 𝐴 ≈ 𝐶 )