Theorem soirri

Description: A strict order relation is irreflexive. (Contributed by NM, 10-Feb-1996) (Revised by Mario Carneiro, 10-May-2013)

	Ref	Expression
Hypotheses	soi.1	$$⊢R\mathrm{Or}S$$
	soi.2	$$⊢R\subseteq S\times S$$
Assertion	soirri	$$⊢\neg ARA$$

Proof

Step	Hyp	Ref	Expression
1		soi.1	$$⊢R\mathrm{Or}S$$
2		soi.2	$$⊢R\subseteq S\times S$$
3		sonr	$$⊢\left(R\mathrm{Or}S\wedge A\in S\right)\to \neg ARA$$
4	1 3	mpan	$$⊢A\in S\to \neg ARA$$
5	4	adantl	$$⊢\left(A\in S\wedge A\in S\right)\to \neg ARA$$
6	2	brel	$$⊢ARA\to \left(A\in S\wedge A\in S\right)$$
7	6	con3i	$$⊢\neg \left(A\in S\wedge A\in S\right)\to \neg ARA$$
8	5 7	pm2.61i	$$⊢\neg ARA$$