Metamath Proof Explorer

Theorem soasym

Description: Asymmetry law for strict orderings. (Contributed by Scott Fenton, 24-Nov-2021)

Ref Expression
Assertion soasym 
|- ( ( R Or A /\ ( X e. A /\ Y e. A ) ) -> ( X R Y -> -. Y R X ) )

Proof

Step Hyp Ref Expression
1 sotric 
 |-  ( ( R Or A /\ ( X e. A /\ Y e. A ) ) -> ( X R Y <-> -. ( X = Y \/ Y R X ) ) )
2 pm2.46 
 |-  ( -. ( X = Y \/ Y R X ) -> -. Y R X )
3 1 2 syl6bi 
 |-  ( ( R Or A /\ ( X e. A /\ Y e. A ) ) -> ( X R Y -> -. Y R X ) )