Theorem poirr

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

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

Proof

Step	Hyp	Ref	Expression
1		df-3an	$$⊢\left(B\in A\wedge B\in A\wedge B\in A\right)\leftrightarrow \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)\leftrightarrow \left(B\in A\wedge B\in A\right)$$
3		anidm	$$⊢\left(B\in A\wedge B\in A\right)\leftrightarrow B\in A$$
4	1 2 3	3bitrri	$$⊢B\in A\leftrightarrow \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(\neg BRB\wedge \left(\left(BRB\wedge BRB\right)\to BRB\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(\neg BRB\wedge \left(\left(BRB\wedge BRB\right)\to BRB\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 \neg BRB$$
8	4 7	sylan2b	$$⊢\left(R\mathrm{Po}A\wedge B\in A\right)\to \neg BRB$$