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

Theorem posref 16245
Description: A poset ordering is reflexive. (Contributed by NM, 11-Sep-2011.) (Proof shortened by OpenAI, 25-Mar-2020.)
Hypotheses
Ref Expression
posi.b  |-  B  =  ( Base `  K
)
posi.l  |-  .<_  =  ( le `  K )
Assertion
Ref Expression
posref  |-  ( ( K  e.  Poset  /\  X  e.  B )  ->  X  .<_  X )

Proof of Theorem posref
StepHypRef Expression
1 posprs 16243 . 2  |-  ( K  e.  Poset  ->  K  e.  Preset  )
2 posi.b . . 3  |-  B  =  ( Base `  K
)
3 posi.l . . 3  |-  .<_  =  ( le `  K )
42, 3prsref 16226 . 2  |-  ( ( K  e.  Preset  /\  X  e.  B )  ->  X  .<_  X )
51, 4sylan 478 1  |-  ( ( K  e.  Poset  /\  X  e.  B )  ->  X  .<_  X )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    = wceq 1455    e. wcel 1898   class class class wbr 4416   ` cfv 5601   Basecbs 15170   lecple 15246    Preset cpreset 16220   Posetcpo 16234
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-nul 4548
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-iota 5565  df-fv 5609  df-preset 16222  df-poset 16240
This theorem is referenced by:  posasymb  16247  pleval2  16260  pltval3  16262  pospo  16268  lublecllem  16283  latref  16348  odupos  16430  omndmul2  28524  omndmul  28526  archirngz  28555  gsumle  28591  cvrnbtwn2  32886  cvrnbtwn3  32887  cvrnbtwn4  32890  cvrcmp  32894  llncmp  33132  lplncmp  33172  lvolcmp  33227
  Copyright terms: Public domain W3C validator