Theorem soasym

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

	Ref	Expression
Assertion	soasym	$$⊢\left(R\mathrm{Or}A\wedge \left(X\in A\wedge Y\in A\right)\right)\to \left(XRY\to \neg YRX\right)$$

Proof

Step	Hyp	Ref	Expression
1		sotric	$$⊢\left(R\mathrm{Or}A\wedge \left(X\in A\wedge Y\in A\right)\right)\to \left(XRY\leftrightarrow \neg \left(X=Y\vee YRX\right)\right)$$
2		pm2.46	$$⊢\neg \left(X=Y\vee YRX\right)\to \neg YRX$$
3	1 2	biimtrdi	$$⊢\left(R\mathrm{Or}A\wedge \left(X\in A\wedge Y\in A\right)\right)\to \left(XRY\to \neg YRX\right)$$