Theorem hlpos 40181

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Posetcpo 18388  Latclat 18512  HLchlt 40165

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-xp 5672  df-dm 5676  df-iota 6499  df-fv 6551  df-ov 7426  df-lat 18513  df-atl 40113  df-cvlat 40137  df-hlat 40166

This theorem is used by:  hlhgt2  40204  hl0lt1N  40205  cvrval3  40228  cvrexchlem  40234  cvratlem  40236  cvrat  40237  atlelt  40253  2atlt  40254  athgt  40271  1cvratex  40288  ps-2  40293  llnnleat  40328  llncmp  40337  2llnmat  40339  lplnnle2at  40356  llncvrlpln  40373  lplncmp  40377  lvolnle3at  40397  lplncvrlvol  40431  lvolcmp  40432  pmaple  40576  2lnat  40599  2atm2atN  40600  lhp2lt  40816  lhp0lt  40818  dia2dimlem2  41880  dia2dimlem3  41881  dih1  42101