Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hlpos Structured version   Unicode version

Theorem hlpos 34180
Description: A Hilbert lattice is a poset. (Contributed by NM, 20-Oct-2011.)
Assertion
Ref Expression
hlpos  |-  ( K  e.  HL  ->  K  e.  Poset )

Proof of Theorem hlpos
StepHypRef Expression
1 hllat 34178 . 2  |-  ( K  e.  HL  ->  K  e.  Lat )
2 latpos 15537 . 2  |-  ( K  e.  Lat  ->  K  e.  Poset )
31, 2syl 16 1  |-  ( K  e.  HL  ->  K  e.  Poset )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767   Posetcpo 15427   Latclat 15532   HLchlt 34165
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-xp 5005  df-dm 5009  df-iota 5551  df-fv 5596  df-ov 6287  df-lat 15533  df-atl 34113  df-cvlat 34137  df-hlat 34166
This theorem is referenced by:  hlhgt2  34203  hl0lt1N  34204  cvrval3  34227  cvrexchlem  34233  cvratlem  34235  cvrat  34236  atlelt  34252  2atlt  34253  athgt  34270  1cvratex  34287  ps-2  34292  llnnleat  34327  llncmp  34336  2llnmat  34338  lplnnle2at  34355  llncvrlpln  34372  lplncmp  34376  lvolnle3at  34396  lplncvrlvol  34430  lvolcmp  34431  pmaple  34575  2lnat  34598  2atm2atN  34599  lhp2lt  34815  lhp0lt  34817  dia2dimlem2  35880  dia2dimlem3  35881  dih1  36101
  Copyright terms: Public domain W3C validator