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

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 \land (X \in A \land Y \in A)) \to (X R Y \to \neg Y R X)$

Step	Hyp	Ref	Expression
1		sotric	$⊢ (R Or A \land (X \in A \land Y \in A)) \to (X R Y \leftrightarrow \neg (X = Y \lor Y R X))$
2		pm2.46	$⊢ \neg (X = Y \lor Y R X) \to \neg Y R X$
3	1 2	biimtrdi	$⊢ (R Or A \land (X \in A \land Y \in A)) \to (X R Y \to \neg Y R X)$