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

Proof

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