Theorem hlop 35949

Description: A Hilbert lattice is an orthoposet. (Contributed by NM, 20-Oct-2011.)

Assertion

Ref	Expression
hlop	⊢ (𝐾 ∈ HL → 𝐾 ∈ OP)

Proof of Theorem hlop

Step	Hyp	Ref	Expression
1		hlol 35948	. 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
2		olop 35801	. 2 ⊢ (𝐾 ∈ OL → 𝐾 ∈ OP)
3	1, 2	syl 17	1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP)

Syntax hints:   → wi 4   ∈ wcel 2050  OPcops 35759  OLcol 35761  HLchlt 35937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3417  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-nul 4179  df-if 4351  df-sn 4442  df-pr 4444  df-op 4448  df-uni 4713  df-br 4930  df-iota 6152  df-fv 6196  df-ov 6979  df-ol 35765  df-oml 35766  df-hlat 35938

This theorem is referenced by:  glbconN  35964  glbconxN  35965  hlhgt2  35976  hl0lt1N  35977  hl2at  35992  cvrexch  36007  atcvr0eq  36013  lnnat  36014  atle  36023  cvrat4  36030  athgt  36043  1cvrco  36059  1cvratex  36060  1cvrjat  36062  1cvrat  36063  ps-2  36065  llnn0  36103  lplnn0N  36134  llncvrlpln  36145  lvoln0N  36178  lplncvrlvol  36203  dalemkeop  36212  pmapeq0  36353  pmapglb2N  36358  pmapglb2xN  36359  2atm2atN  36372  polval2N  36493  polsubN  36494  pol1N  36497  2polpmapN  36500  2polvalN  36501  poldmj1N  36515  pmapj2N  36516  2polatN  36519  pnonsingN  36520  ispsubcl2N  36534  polsubclN  36539  poml4N  36540  pmapojoinN  36555  pl42lem1N  36566  lhp2lt  36588  lhp0lt  36590  lhpn0  36591  lhpexnle  36593  lhpoc2N  36602  lhpocnle  36603  lhpj1  36609  lhpmod2i2  36625  lhpmod6i1  36626  lhprelat3N  36627  ltrnatb  36724  trlcl  36751  trlle  36771  cdleme3c  36817  cdleme7e  36834  cdleme22b  36928  cdlemg12e  37234  cdlemg12g  37236  tendoid  37360  tendo0tp  37376  cdlemk39s-id  37527  tendoex  37562  dia0eldmN  37627  dia2dimlem2  37652  dia2dimlem3  37653  docaclN  37711  doca2N  37713  djajN  37724  dib0  37751  dih0  37867  dih0bN  37868  dih0rn  37871  dih1  37873  dih1rn  37874  dih1cnv  37875  dihmeetlem18N  37911  dih1dimatlem  37916  dihlspsnssN  37919  dihlspsnat  37920  dihatexv  37925  dihglb2  37929  dochcl  37940  doch0  37945  doch1  37946  dochvalr3  37950  doch2val2  37951  dochss  37952  dochocss  37953  dochoc  37954  dochnoncon  37978  djhlj  37988  dihjatc  38004