Metamath Proof Explorer


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