Theorem hlpos 40516

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Posetcpo 18486  Latclat 18610  HLchlt 40500

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-xp 5656  df-dm 5660  df-iota 6494  df-fv 6546  df-ov 7423  df-lat 18611  df-atl 40448  df-cvlat 40472  df-hlat 40501

This theorem is used by:  hlhgt2  40539  hl0lt1N  40540  cvrval3  40563  cvrexchlem  40569  cvratlem  40571  cvrat  40572  atlelt  40588  2atlt  40589  athgt  40606  1cvratex  40623  ps-2  40628  llnnleat  40663  llncmp  40672  2llnmat  40674  lplnnle2at  40691  llncvrlpln  40708  lplncmp  40712  lvolnle3at  40732  lplncvrlvol  40766  lvolcmp  40767  pmaple  40911  2lnat  40934  2atm2atN  40935  lhp2lt  41151  lhp0lt  41153  dia2dimlem2  42215  dia2dimlem3  42216  dih1  42436