Metamath Proof Explorer

Theorem poirr

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

Ref Expression
Assertion poirr ⊢ R Po A ∧ B ∈ A → ¬ B R B

Proof

Step Hyp Ref Expression
1 df-3an ⊢ B ∈ A ∧ B ∈ A ∧ B ∈ A ↔ B ∈ A ∧ B ∈ A ∧ B ∈ A
2 anabs1 ⊢ B ∈ A ∧ B ∈ A ∧ B ∈ A ↔ B ∈ A ∧ B ∈ A
3 anidm ⊢ B ∈ A ∧ B ∈ A ↔ B ∈ A
4 1 2 3 3bitrri ⊢ B ∈ A ↔ B ∈ A ∧ B ∈ A ∧ B ∈ A
5 pocl ⊢ R Po A → B ∈ A ∧ B ∈ A ∧ B ∈ A → ¬ B R B ∧ B R B ∧ B R B → B R B
6 5 imp ⊢ R Po A ∧ B ∈ A ∧ B ∈ A ∧ B ∈ A → ¬ B R B ∧ B R B ∧ B R B → B R B
7 6 simpld ⊢ R Po A ∧ B ∈ A ∧ B ∈ A ∧ B ∈ A → ¬ B R B
8 4 7 sylan2b ⊢ R Po A ∧ B ∈ A → ¬ B R B