Theorem hlpos 35379

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

Syntax hints:   → wi 4   ∈ wcel 2157  Posetcpo 17252  Latclat 17357  HLchlt 35363

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2354  ax-ext 2775

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-ne 2970  df-ral 3092  df-rex 3093  df-rab 3096  df-v 3385  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-nul 4114  df-if 4276  df-sn 4367  df-pr 4369  df-op 4373  df-uni 4627  df-br 4842  df-opab 4904  df-xp 5316  df-dm 5320  df-iota 6062  df-fv 6107  df-ov 6879  df-lat 17358  df-atl 35311  df-cvlat 35335  df-hlat 35364

This theorem is referenced by:  hlhgt2  35402  hl0lt1N  35403  cvrval3  35426  cvrexchlem  35432  cvratlem  35434  cvrat  35435  atlelt  35451  2atlt  35452  athgt  35469  1cvratex  35486  ps-2  35491  llnnleat  35526  llncmp  35535  2llnmat  35537  lplnnle2at  35554  llncvrlpln  35571  lplncmp  35575  lvolnle3at  35595  lplncvrlvol  35629  lvolcmp  35630  pmaple  35774  2lnat  35797  2atm2atN  35798  lhp2lt  36014  lhp0lt  36016  dia2dimlem2  37078  dia2dimlem3  37079  dih1  37299