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 |
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 |