MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  poirr Structured version   Visualization version   GIF version

Theorem poirr 5591
Description: A partial order is irreflexive. (Contributed by NM, 27-Mar-1997.)
Assertion
Ref Expression
poirr ((𝑅 Po 𝐴𝐵𝐴) → ¬ 𝐵𝑅𝐵)

Proof of Theorem poirr
StepHypRef Expression
1 df-3an 1086 . . 3 ((𝐵𝐴𝐵𝐴𝐵𝐴) ↔ ((𝐵𝐴𝐵𝐴) ∧ 𝐵𝐴))
2 anabs1 659 . . 3 (((𝐵𝐴𝐵𝐴) ∧ 𝐵𝐴) ↔ (𝐵𝐴𝐵𝐴))
3 anidm 564 . . 3 ((𝐵𝐴𝐵𝐴) ↔ 𝐵𝐴)
41, 2, 33bitrri 298 . 2 (𝐵𝐴 ↔ (𝐵𝐴𝐵𝐴𝐵𝐴))
5 pocl 5586 . . . 4 (𝑅 Po 𝐴 → ((𝐵𝐴𝐵𝐴𝐵𝐴) → (¬ 𝐵𝑅𝐵 ∧ ((𝐵𝑅𝐵𝐵𝑅𝐵) → 𝐵𝑅𝐵))))
65imp 406 . . 3 ((𝑅 Po 𝐴 ∧ (𝐵𝐴𝐵𝐴𝐵𝐴)) → (¬ 𝐵𝑅𝐵 ∧ ((𝐵𝑅𝐵𝐵𝑅𝐵) → 𝐵𝑅𝐵)))
76simpld 494 . 2 ((𝑅 Po 𝐴 ∧ (𝐵𝐴𝐵𝐴𝐵𝐴)) → ¬ 𝐵𝑅𝐵)
84, 7sylan2b 593 1 ((𝑅 Po 𝐴𝐵𝐴) → ¬ 𝐵𝑅𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  w3a 1084  wcel 2098   class class class wbr 5139   Po wpo 5577
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-ral 3054  df-rab 3425  df-v 3468  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4522  df-sn 4622  df-pr 4624  df-op 4628  df-br 5140  df-po 5579
This theorem is referenced by:  po2nr  5593  po2ne  5595  pofun  5597  sonr  5602  poirr2  6116  predpoirr  6325  soisoi  7318  poxp  8109  poseq  8139  swoer  8730  frfi  9285  wemappo  9541  zorn2lem3  10490  ex-po  30182  pocnv  35255  epirron  42552  ipo0  43757
  Copyright terms: Public domain W3C validator