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

Theorem posref 17266
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 17264 . 2 (𝐾 ∈ Poset → 𝐾 ∈ Proset )
2 posi.b . . 3 𝐵 = (Base‘𝐾)
3 posi.l . . 3 = (le‘𝐾)
42, 3prsref 17247 . 2 ((𝐾 ∈ Proset ∧ 𝑋𝐵) → 𝑋 𝑋)
51, 4sylan 576 1 ((𝐾 ∈ Poset ∧ 𝑋𝐵) → 𝑋 𝑋)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385   = wceq 1653  wcel 2157   class class class wbr 4843  cfv 6101  Basecbs 16184  lecple 16274   Proset cproset 17241  Posetcpo 17255
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777  ax-nul 4983
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3387  df-sbc 3634  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4116  df-if 4278  df-sn 4369  df-pr 4371  df-op 4375  df-uni 4629  df-br 4844  df-iota 6064  df-fv 6109  df-proset 17243  df-poset 17261
This theorem is referenced by:  posasymb  17267  pleval2  17280  pltval3  17282  pospo  17288  lublecllem  17303  latref  17368  odupos  17450  omndmul2  30228  omndmul  30230  archirngz  30259  gsumle  30295  cvrnbtwn2  35296  cvrnbtwn3  35297  cvrnbtwn4  35300  cvrcmp  35304  llncmp  35543  lplncmp  35583  lvolcmp  35638
  Copyright terms: Public domain W3C validator