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 )