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

Theorem posref 16720
Description: A poset ordering is reflexive. (Contributed by NM, 11-Sep-2011.) (Proof shortened by OpenAI, 25-Mar-2020.)
Hypotheses
Ref Expression
posi.b 𝐵 = (Base‘𝐾)
posi.l = (le‘𝐾)
Assertion
Ref Expression
posref ((𝐾 ∈ Poset ∧ 𝑋𝐵) → 𝑋 𝑋)

Proof of Theorem posref
StepHypRef Expression
1 posprs 16718 . 2 (𝐾 ∈ Poset → 𝐾 ∈ Preset )
2 posi.b . . 3 𝐵 = (Base‘𝐾)
3 posi.l . . 3 = (le‘𝐾)
42, 3prsref 16701 . 2 ((𝐾 ∈ Preset ∧ 𝑋𝐵) → 𝑋 𝑋)
51, 4sylan 486 1 ((𝐾 ∈ Poset ∧ 𝑋𝐵) → 𝑋 𝑋)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wcel 1976   class class class wbr 4577  cfv 5790  Basecbs 15641  lecple 15721   Preset cpreset 16695  Posetcpo 16709
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-nul 4712
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-iota 5754  df-fv 5798  df-preset 16697  df-poset 16715
This theorem is referenced by:  posasymb  16721  pleval2  16734  pltval3  16736  pospo  16742  lublecllem  16757  latref  16822  odupos  16904  omndmul2  28849  omndmul  28851  archirngz  28880  gsumle  28916  cvrnbtwn2  33376  cvrnbtwn3  33377  cvrnbtwn4  33380  cvrcmp  33384  llncmp  33622  lplncmp  33662  lvolcmp  33717
  Copyright terms: Public domain W3C validator