This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ¬ 𝐵 𝑅 𝐵 )