Theorem hlpos 36662

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

Syntax hints:   → wi 4   ∈ wcel 2111  Posetcpo 17542  Latclat 17647  HLchlt 36646

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-xp 5525  df-dm 5529  df-iota 6283  df-fv 6332  df-ov 7138  df-lat 17648  df-atl 36594  df-cvlat 36618  df-hlat 36647

This theorem is referenced by:  hlhgt2  36685  hl0lt1N  36686  cvrval3  36709  cvrexchlem  36715  cvratlem  36717  cvrat  36718  atlelt  36734  2atlt  36735  athgt  36752  1cvratex  36769  ps-2  36774  llnnleat  36809  llncmp  36818  2llnmat  36820  lplnnle2at  36837  llncvrlpln  36854  lplncmp  36858  lvolnle3at  36878  lplncvrlvol  36912  lvolcmp  36913  pmaple  37057  2lnat  37080  2atm2atN  37081  lhp2lt  37297  lhp0lt  37299  dia2dimlem2  38361  dia2dimlem3  38362  dih1  38582