Theorem hlpos 40118

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

Syntax hints:   → wi 4   ∈ wcel 2143  Posetcpo 18364  Latclat 18488  HLchlt 40102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-xp 5669  df-dm 5673  df-iota 6494  df-fv 6546  df-ov 7415  df-lat 18489  df-atl 40050  df-cvlat 40074  df-hlat 40103

This theorem is referenced by:  hlhgt2  40141  hl0lt1N  40142  cvrval3  40165  cvrexchlem  40171  cvratlem  40173  cvrat  40174  atlelt  40190  2atlt  40191  athgt  40208  1cvratex  40225  ps-2  40230  llnnleat  40265  llncmp  40274  2llnmat  40276  lplnnle2at  40293  llncvrlpln  40310  lplncmp  40314  lvolnle3at  40334  lplncvrlvol  40368  lvolcmp  40369  pmaple  40513  2lnat  40536  2atm2atN  40537  lhp2lt  40753  lhp0lt  40755  dia2dimlem2  41817  dia2dimlem3  41818  dih1  42038