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

Theorem hlpos 36504
Description: A Hilbert lattice is a poset. (Contributed by NM, 20-Oct-2011.)
Assertion
Ref Expression
hlpos (𝐾 ∈ HL → 𝐾 ∈ Poset)

Proof of Theorem hlpos
StepHypRef Expression
1 hllat 36501 . 2 (𝐾 ∈ HL → 𝐾 ∈ Lat)
2 latpos 17662 . 2 (𝐾 ∈ Lat → 𝐾 ∈ Poset)
31, 2syl 17 1 (𝐾 ∈ HL → 𝐾 ∈ Poset)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2114  Posetcpo 17552  Latclat 17657  HLchlt 36488
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-xp 5563  df-dm 5567  df-iota 6316  df-fv 6365  df-ov 7161  df-lat 17658  df-atl 36436  df-cvlat 36460  df-hlat 36489
This theorem is referenced by:  hlhgt2  36527  hl0lt1N  36528  cvrval3  36551  cvrexchlem  36557  cvratlem  36559  cvrat  36560  atlelt  36576  2atlt  36577  athgt  36594  1cvratex  36611  ps-2  36616  llnnleat  36651  llncmp  36660  2llnmat  36662  lplnnle2at  36679  llncvrlpln  36696  lplncmp  36700  lvolnle3at  36720  lplncvrlvol  36754  lvolcmp  36755  pmaple  36899  2lnat  36922  2atm2atN  36923  lhp2lt  37139  lhp0lt  37141  dia2dimlem2  38203  dia2dimlem3  38204  dih1  38424
  Copyright terms: Public domain W3C validator