Metamath Proof Explorer

Theorem domtrfir

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

Ref Expression
Assertion domtrfir ⊢ C ∈ Fin ∧ A ≼ B ∧ B ≼ C → A ≼ C

Proof

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