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 S × S
Assertion soirri ¬ A R A

Proof

Step Hyp Ref Expression
1 soi.1 R Or S
2 soi.2 R S × S
3 sonr R Or S A S ¬ A R A
4 1 3 mpan A S ¬ A R A
5 4 adantl A S A S ¬ A R A
6 2 brel A R A A S A S
7 6 con3i ¬ A S A S ¬ A R A
8 5 7 pm2.61i ¬ A R A