Theorem hlpos 40391

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Posetcpo 18461  Latclat 18585  HLchlt 40375

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 2147  ax-9 2155  ax-ext 2733

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 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-xp 5657  df-dm 5661  df-iota 6487  df-fv 6539  df-ov 7415  df-lat 18586  df-atl 40323  df-cvlat 40347  df-hlat 40376

This theorem is used by:  hlhgt2  40414  hl0lt1N  40415  cvrval3  40438  cvrexchlem  40444  cvratlem  40446  cvrat  40447  atlelt  40463  2atlt  40464  athgt  40481  1cvratex  40498  ps-2  40503  llnnleat  40538  llncmp  40547  2llnmat  40549  lplnnle2at  40566  llncvrlpln  40583  lplncmp  40587  lvolnle3at  40607  lplncvrlvol  40641  lvolcmp  40642  pmaple  40786  2lnat  40809  2atm2atN  40810  lhp2lt  41026  lhp0lt  41028  dia2dimlem2  42090  dia2dimlem3  42091  dih1  42311