Theorem poirr

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

	Ref	Expression
Assertion	poirr	⊢ ( ( 𝑅 Po 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ¬ 𝐵 𝑅 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		df-3an	⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐵 ∈ 𝐴 ) ↔ ( ( 𝐵 ∈ 𝐴 ∧ 𝐵 ∈ 𝐴 ) ∧ 𝐵 ∈ 𝐴 ) )
2		anabs1	⊢ ( ( ( 𝐵 ∈ 𝐴 ∧ 𝐵 ∈ 𝐴 ) ∧ 𝐵 ∈ 𝐴 ) ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐵 ∈ 𝐴 ) )
3		anidm	⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝐵 ∈ 𝐴 ) ↔ 𝐵 ∈ 𝐴 )
4	1 2 3	3bitrri	⊢ ( 𝐵 ∈ 𝐴 ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐵 ∈ 𝐴 ) )
5		pocl	⊢ ( 𝑅 Po 𝐴 → ( ( 𝐵 ∈ 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( ¬ 𝐵 𝑅 𝐵 ∧ ( ( 𝐵 𝑅 𝐵 ∧ 𝐵 𝑅 𝐵 ) → 𝐵 𝑅 𝐵 ) ) ) )
6	5	imp	⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐵 ∈ 𝐴 ) ) → ( ¬ 𝐵 𝑅 𝐵 ∧ ( ( 𝐵 𝑅 𝐵 ∧ 𝐵 𝑅 𝐵 ) → 𝐵 𝑅 𝐵 ) ) )
7	6	simpld	⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐵 ∈ 𝐴 ) ) → ¬ 𝐵 𝑅 𝐵 )
8	4 7	sylan2b	⊢ ( ( 𝑅 Po 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ¬ 𝐵 𝑅 𝐵 )