Theorem poirr

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

	Ref	Expression
Assertion	poirr	|- ( ( R Po A /\ B e. A ) -> -. B R B )

Proof

Step	Hyp	Ref	Expression
1		df-3an	|- ( ( B e. A /\ B e. A /\ B e. A ) <-> ( ( B e. A /\ B e. A ) /\ B e. A ) )
2		anabs1	|- ( ( ( B e. A /\ B e. A ) /\ B e. A ) <-> ( B e. A /\ B e. A ) )
3		anidm	|- ( ( B e. A /\ B e. A ) <-> B e. A )
4	1 2 3	3bitrri	|- ( B e. A <-> ( B e. A /\ B e. A /\ B e. A ) )
5		pocl	|- ( R Po A -> ( ( B e. A /\ B e. A /\ B e. A ) -> ( -. B R B /\ ( ( B R B /\ B R B ) -> B R B ) ) ) )
6	5	imp	|- ( ( R Po A /\ ( B e. A /\ B e. A /\ B e. A ) ) -> ( -. B R B /\ ( ( B R B /\ B R B ) -> B R B ) ) )
7	6	simpld	|- ( ( R Po A /\ ( B e. A /\ B e. A /\ B e. A ) ) -> -. B R B )
8	4 7	sylan2b	|- ( ( R Po A /\ B e. A ) -> -. B R B )