This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sdomn2lp

Description: Strict dominance has no 2-cycle loops. (Contributed by NM, 6-May-2008)

Ref Expression
Assertion sdomn2lp ⊢ ¬ A ≺ B ∧ B ≺ A

Proof

Step Hyp Ref Expression
1 sdomirr ⊢ ¬ A ≺ A
2 sdomtr ⊢ A ≺ B ∧ B ≺ A → A ≺ A
3 1 2 mto ⊢ ¬ A ≺ B ∧ B ≺ A