# Metamath Proof Explorer

## Theorem poirr

Description: A partial order relation is irreflexive. (Contributed by NM, 27-Mar-1997)

Ref Expression
Assertion poirr ${⊢}\left({R}\mathrm{Po}{A}\wedge {B}\in {A}\right)\to ¬{B}{R}{B}$

### Proof

Step Hyp Ref Expression
1 df-3an ${⊢}\left({B}\in {A}\wedge {B}\in {A}\wedge {B}\in {A}\right)↔\left(\left({B}\in {A}\wedge {B}\in {A}\right)\wedge {B}\in {A}\right)$
2 anabs1 ${⊢}\left(\left({B}\in {A}\wedge {B}\in {A}\right)\wedge {B}\in {A}\right)↔\left({B}\in {A}\wedge {B}\in {A}\right)$
3 anidm ${⊢}\left({B}\in {A}\wedge {B}\in {A}\right)↔{B}\in {A}$
4 1 2 3 3bitrri ${⊢}{B}\in {A}↔\left({B}\in {A}\wedge {B}\in {A}\wedge {B}\in {A}\right)$
5 pocl ${⊢}{R}\mathrm{Po}{A}\to \left(\left({B}\in {A}\wedge {B}\in {A}\wedge {B}\in {A}\right)\to \left(¬{B}{R}{B}\wedge \left(\left({B}{R}{B}\wedge {B}{R}{B}\right)\to {B}{R}{B}\right)\right)\right)$
6 5 imp ${⊢}\left({R}\mathrm{Po}{A}\wedge \left({B}\in {A}\wedge {B}\in {A}\wedge {B}\in {A}\right)\right)\to \left(¬{B}{R}{B}\wedge \left(\left({B}{R}{B}\wedge {B}{R}{B}\right)\to {B}{R}{B}\right)\right)$
7 6 simpld ${⊢}\left({R}\mathrm{Po}{A}\wedge \left({B}\in {A}\wedge {B}\in {A}\wedge {B}\in {A}\right)\right)\to ¬{B}{R}{B}$
8 4 7 sylan2b ${⊢}\left({R}\mathrm{Po}{A}\wedge {B}\in {A}\right)\to ¬{B}{R}{B}$