Theorem hlpos 39344

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 39341	. 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
2		latpos 18362	. 2 ⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset)
3	1, 2	syl 17	1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset)

Syntax hints:   → wi 4   ∈ wcel 2109  Posetcpo 18231  Latclat 18355  HLchlt 39328

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-xp 5629  df-dm 5633  df-iota 6442  df-fv 6494  df-ov 7356  df-lat 18356  df-atl 39276  df-cvlat 39300  df-hlat 39329

This theorem is referenced by:  hlhgt2  39368  hl0lt1N  39369  cvrval3  39392  cvrexchlem  39398  cvratlem  39400  cvrat  39401  atlelt  39417  2atlt  39418  athgt  39435  1cvratex  39452  ps-2  39457  llnnleat  39492  llncmp  39501  2llnmat  39503  lplnnle2at  39520  llncvrlpln  39537  lplncmp  39541  lvolnle3at  39561  lplncvrlvol  39595  lvolcmp  39596  pmaple  39740  2lnat  39763  2atm2atN  39764  lhp2lt  39980  lhp0lt  39982  dia2dimlem2  41044  dia2dimlem3  41045  dih1  41265