Theorem hlpos 37380

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

Syntax hints:   → wi 4   ∈ wcel 2106  Posetcpo 18025  Latclat 18149  HLchlt 37364

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-xp 5595  df-dm 5599  df-iota 6391  df-fv 6441  df-ov 7278  df-lat 18150  df-atl 37312  df-cvlat 37336  df-hlat 37365

This theorem is referenced by:  hlhgt2  37403  hl0lt1N  37404  cvrval3  37427  cvrexchlem  37433  cvratlem  37435  cvrat  37436  atlelt  37452  2atlt  37453  athgt  37470  1cvratex  37487  ps-2  37492  llnnleat  37527  llncmp  37536  2llnmat  37538  lplnnle2at  37555  llncvrlpln  37572  lplncmp  37576  lvolnle3at  37596  lplncvrlvol  37630  lvolcmp  37631  pmaple  37775  2lnat  37798  2atm2atN  37799  lhp2lt  38015  lhp0lt  38017  dia2dimlem2  39079  dia2dimlem3  39080  dih1  39300