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

Theorem poirr 5609
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 1088 . . 3 ((𝐵𝐴𝐵𝐴𝐵𝐴) ↔ ((𝐵𝐴𝐵𝐴) ∧ 𝐵𝐴))
2 anabs1 662 . . 3 (((𝐵𝐴𝐵𝐴) ∧ 𝐵𝐴) ↔ (𝐵𝐴𝐵𝐴))
3 anidm 564 . . 3 ((𝐵𝐴𝐵𝐴) ↔ 𝐵𝐴)
41, 2, 33bitrri 298 . 2 (𝐵𝐴 ↔ (𝐵𝐴𝐵𝐴𝐵𝐴))
5 pocl 5605 . . . 4 (𝑅 Po 𝐴 → ((𝐵𝐴𝐵𝐴𝐵𝐴) → (¬ 𝐵𝑅𝐵 ∧ ((𝐵𝑅𝐵𝐵𝑅𝐵) → 𝐵𝑅𝐵))))
65imp 406 . . 3 ((𝑅 Po 𝐴 ∧ (𝐵𝐴𝐵𝐴𝐵𝐴)) → (¬ 𝐵𝑅𝐵 ∧ ((𝐵𝑅𝐵𝐵𝑅𝐵) → 𝐵𝑅𝐵)))
76simpld 494 . 2 ((𝑅 Po 𝐴 ∧ (𝐵𝐴𝐵𝐴𝐵𝐴)) → ¬ 𝐵𝑅𝐵)
84, 7sylan2b 594 1 ((𝑅 Po 𝐴𝐵𝐴) → ¬ 𝐵𝑅𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  w3a 1086  wcel 2106   class class class wbr 5148   Po wpo 5595
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-po 5597
This theorem is referenced by:  po2nr  5611  po2ne  5613  pofun  5615  sonr  5621  poirr2  6147  predpoirr  6356  soisoi  7348  poxp  8152  poseq  8182  swoer  8775  frfi  9319  wemappo  9587  zorn2lem3  10536  ex-po  30464  pocnv  35743  weiunpo  36448  epirron  43243  ipo0  44445
  Copyright terms: Public domain W3C validator