Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  olop Structured version   Unicode version

Theorem olop 30086
Description: An ortholattice is an orthoposet. (Contributed by NM, 18-Sep-2011.)
Assertion
Ref Expression
olop  |-  ( K  e.  OL  ->  K  e.  OP )

Proof of Theorem olop
StepHypRef Expression
1 isolat 30084 . 2  |-  ( K  e.  OL  <->  ( K  e.  Lat  /\  K  e.  OP ) )
21simprbi 452 1  |-  ( K  e.  OL  ->  K  e.  OP )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726   Latclat 14479   OPcops 30044   OLcol 30046
This theorem is referenced by:  olposN  30087  oldmm1  30089  oldmm2  30090  oldmm3N  30091  oldmm4  30092  oldmj1  30093  oldmj2  30094  oldmj3  30095  oldmj4  30096  olj01  30097  olj02  30098  olm11  30099  olm12  30100  latmassOLD  30101  olm01  30108  olm02  30109  omlop  30113  meetat  30168  hlop  30234  polatN  30802
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-in 3329  df-ol 30050
  Copyright terms: Public domain W3C validator