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

Theorem latref 14410
Description: A lattice ordering is reflexive. (ssid 3311 analog.) (Contributed by NM, 8-Oct-2011.)
Hypotheses
Ref Expression
latref.b  |-  B  =  ( Base `  K
)
latref.l  |-  .<_  =  ( le `  K )
Assertion
Ref Expression
latref  |-  ( ( K  e.  Lat  /\  X  e.  B )  ->  X  .<_  X )

Proof of Theorem latref
StepHypRef Expression
1 latpos 14406 . 2  |-  ( K  e.  Lat  ->  K  e.  Poset )
2 latref.b . . 3  |-  B  =  ( Base `  K
)
3 latref.l . . 3  |-  .<_  =  ( le `  K )
42, 3posref 14336 . 2  |-  ( ( K  e.  Poset  /\  X  e.  B )  ->  X  .<_  X )
51, 4sylan 458 1  |-  ( ( K  e.  Lat  /\  X  e.  B )  ->  X  .<_  X )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649    e. wcel 1717   class class class wbr 4154   ` cfv 5395   Basecbs 13397   lecple 13464   Posetcpo 14325   Latclat 14402
This theorem is referenced by:  latleeqj1  14420  latjidm  14431  latleeqm1  14436  latmidm  14443  olj01  29341  olm01  29352  cmtidN  29373  ps-1  29592  3at  29605  llnneat  29629  2atnelpln  29659  lplnneat  29660  lplnnelln  29661  3atnelvolN  29701  lvolneatN  29703  lvolnelln  29704  lvolnelpln  29705  4at  29728  lplncvrlvol  29731  lncmp  29898  lhpocnle  30131  ltrnel  30254  ltrncnvel  30257  ltrnmw  30266  tendoidcl  30884  cdlemk39u  31083  dia1eldmN  31157  dia1N  31169  dihwN  31405  dihglblem5apreN  31407  dihmeetbclemN  31420
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369  ax-nul 4280
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2243  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-ne 2553  df-ral 2655  df-rex 2656  df-rab 2659  df-v 2902  df-sbc 3106  df-dif 3267  df-un 3269  df-in 3271  df-ss 3278  df-nul 3573  df-if 3684  df-sn 3764  df-pr 3765  df-op 3767  df-uni 3959  df-br 4155  df-iota 5359  df-fv 5403  df-ov 6024  df-poset 14331  df-lat 14403
  Copyright terms: Public domain W3C validator