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 Or S
	soi.2	|- R C_ ( S X. S )
Assertion	soirri	|- -. A R A

Proof

Step	Hyp	Ref	Expression
1		soi.1	|- R Or S
2		soi.2	|- R C_ ( S X. S )
3		sonr	|- ( ( R Or S /\ A e. S ) -> -. A R A )
4	1 3	mpan	|- ( A e. S -> -. A R A )
5	4	adantl	|- ( ( A e. S /\ A e. S ) -> -. A R A )
6	2	brel	|- ( A R A -> ( A e. S /\ A e. S ) )
7	6	con3i	|- ( -. ( A e. S /\ A e. S ) -> -. A R A )
8	5 7	pm2.61i	|- -. A R A