Theorem hlpos 39485

Description: A Hilbert lattice is a poset. (Contributed by NM, 20-Oct-2011.)

Assertion

Ref	Expression
hlpos	⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset)

Proof of Theorem hlpos

Step	Hyp	Ref	Expression
1		hllat 39482	. 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
2		latpos 18346	. 2 ⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset)
3	1, 2	syl 17	1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset)

Syntax hints:   → wi 4   ∈ wcel 2113  Posetcpo 18215  Latclat 18339  HLchlt 39469

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-xp 5625  df-dm 5629  df-iota 6442  df-fv 6494  df-ov 7355  df-lat 18340  df-atl 39417  df-cvlat 39441  df-hlat 39470

This theorem is referenced by:  hlhgt2  39508  hl0lt1N  39509  cvrval3  39532  cvrexchlem  39538  cvratlem  39540  cvrat  39541  atlelt  39557  2atlt  39558  athgt  39575  1cvratex  39592  ps-2  39597  llnnleat  39632  llncmp  39641  2llnmat  39643  lplnnle2at  39660  llncvrlpln  39677  lplncmp  39681  lvolnle3at  39701  lplncvrlvol  39735  lvolcmp  39736  pmaple  39880  2lnat  39903  2atm2atN  39904  lhp2lt  40120  lhp0lt  40122  dia2dimlem2  41184  dia2dimlem3  41185  dih1  41405