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 ∈ Fin ∧ A ≼ B ∧ B ≼ C → A ≼ C

Proof

Step Hyp Ref Expression
1 domfi ⊢ B ∈ Fin ∧ A ≼ B → A ∈ Fin
2 1 3adant3 ⊢ B ∈ Fin ∧ A ≼ B ∧ B ≼ C → A ∈ Fin
3 domtrfil ⊢ A ∈ Fin ∧ A ≼ B ∧ B ≼ C → A ≼ C
4 2 3 syld3an1 ⊢ B ∈ Fin ∧ A ≼ B ∧ B ≼ C → A ≼ C