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

Theorem hlpos 33007
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 33005 . 2  |-  ( K  e.  HL  ->  K  e.  Lat )
2 latpos 15218 . 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 1756   Posetcpo 15108   Latclat 15213   HLchlt 32992
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-dif 3329  df-un 3331  df-in 3333  df-ss 3340  df-nul 3636  df-if 3790  df-sn 3876  df-pr 3878  df-op 3882  df-uni 4090  df-br 4291  df-opab 4349  df-xp 4844  df-dm 4848  df-iota 5379  df-fv 5424  df-ov 6092  df-lat 15214  df-atl 32940  df-cvlat 32964  df-hlat 32993
This theorem is referenced by:  hlhgt2  33030  hl0lt1N  33031  cvrval3  33054  cvrexchlem  33060  cvratlem  33062  cvrat  33063  atlelt  33079  2atlt  33080  athgt  33097  1cvratex  33114  ps-2  33119  llnnleat  33154  llncmp  33163  2llnmat  33165  lplnnle2at  33182  llncvrlpln  33199  lplncmp  33203  lvolnle3at  33223  lplncvrlvol  33257  lvolcmp  33258  pmaple  33402  2lnat  33425  2atm2atN  33426  lhp2lt  33642  lhp0lt  33644  dia2dimlem2  34707  dia2dimlem3  34708  dih1  34928
  Copyright terms: Public domain W3C validator