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

Theorem postr 17851
Description: A poset ordering is transitive. (Contributed by NM, 11-Sep-2011.)
Hypotheses
Ref Expression
posi.b 𝐵 = (Base‘𝐾)
posi.l = (le‘𝐾)
Assertion
Ref Expression
postr ((𝐾 ∈ Poset ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 𝑌𝑌 𝑍) → 𝑋 𝑍))

Proof of Theorem postr
StepHypRef Expression
1 posi.b . . 3 𝐵 = (Base‘𝐾)
2 posi.l . . 3 = (le‘𝐾)
31, 2posi 17848 . 2 ((𝐾 ∈ Poset ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋 𝑋 ∧ ((𝑋 𝑌𝑌 𝑋) → 𝑋 = 𝑌) ∧ ((𝑋 𝑌𝑌 𝑍) → 𝑋 𝑍)))
43simp3d 1146 1 ((𝐾 ∈ Poset ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 𝑌𝑌 𝑍) → 𝑋 𝑍))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1089   = wceq 1543  wcel 2111   class class class wbr 5067  cfv 6397  Basecbs 16784  lecple 16833  Posetcpo 17838
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-nul 5213
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3067  df-rex 3068  df-rab 3071  df-v 3422  df-dif 3883  df-un 3885  df-in 3887  df-ss 3897  df-nul 4252  df-if 4454  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4834  df-br 5068  df-iota 6355  df-fv 6405  df-poset 17844
This theorem is referenced by:  odupos  17858  plttr  17872  joinle  17916  meetle  17930  lattr  17974  omndadd2d  31077  omndadd2rd  31078  omndmul2  31081  atlatle  37097  cvratlem  37198  llncmp  37299  llncvrlpln  37335  lplncmp  37339  lplncvrlvol  37393  lvolcmp  37394  pmaple  37538
  Copyright terms: Public domain W3C validator