Theorem hlpos 37901

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

Syntax hints:   → wi 4   ∈ wcel 2106  Posetcpo 18210  Latclat 18334  HLchlt 37885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-xp 5644  df-dm 5648  df-iota 6453  df-fv 6509  df-ov 7365  df-lat 18335  df-atl 37833  df-cvlat 37857  df-hlat 37886

This theorem is referenced by:  hlhgt2  37925  hl0lt1N  37926  cvrval3  37949  cvrexchlem  37955  cvratlem  37957  cvrat  37958  atlelt  37974  2atlt  37975  athgt  37992  1cvratex  38009  ps-2  38014  llnnleat  38049  llncmp  38058  2llnmat  38060  lplnnle2at  38077  llncvrlpln  38094  lplncmp  38098  lvolnle3at  38118  lplncvrlvol  38152  lvolcmp  38153  pmaple  38297  2lnat  38320  2atm2atN  38321  lhp2lt  38537  lhp0lt  38539  dia2dimlem2  39601  dia2dimlem3  39602  dih1  39822