Metamath Proof Explorer

Theorem domtrfi

Description: Transitivity of dominance relation when B is finite, proved without using the Axiom of Power Sets (unlike domtr ). (Contributed by BTernaryTau, 24-Nov-2024)

		Ref	Expression
	Assertion	domtrfi	$⊢ (B \in Fin \land A ≼ B \land B ≼ C) \to A ≼ C$

Proof

Step	Hyp	Ref	Expression
1		domfi	$⊢ (B \in Fin \land A ≼ B) \to A \in Fin$
2	1	3adant3	$⊢ (B \in Fin \land A ≼ B \land B ≼ C) \to A \in Fin$
3		domtrfil	$⊢ (A \in Fin \land A ≼ B \land B ≼ C) \to A ≼ C$
4	2 3	syld3an1	$⊢ (B \in Fin \land A ≼ B \land B ≼ C) \to A ≼ C$