Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  omlol Structured version   Visualization version   GIF version

Theorem omlol 36535
 Description: An orthomodular lattice is an ortholattice. (Contributed by NM, 18-Sep-2011.)
Assertion
Ref Expression
omlol (𝐾 ∈ OML → 𝐾 ∈ OL)

Proof of Theorem omlol
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2801 . . 3 (Base‘𝐾) = (Base‘𝐾)
2 eqid 2801 . . 3 (le‘𝐾) = (le‘𝐾)
3 eqid 2801 . . 3 (join‘𝐾) = (join‘𝐾)
4 eqid 2801 . . 3 (meet‘𝐾) = (meet‘𝐾)
5 eqid 2801 . . 3 (oc‘𝐾) = (oc‘𝐾)
61, 2, 3, 4, 5isoml 36533 . 2 (𝐾 ∈ OML ↔ (𝐾 ∈ OL ∧ ∀𝑥 ∈ (Base‘𝐾)∀𝑦 ∈ (Base‘𝐾)(𝑥(le‘𝐾)𝑦𝑦 = (𝑥(join‘𝐾)(𝑦(meet‘𝐾)((oc‘𝐾)‘𝑥))))))
76simplbi 501 1 (𝐾 ∈ OML → 𝐾 ∈ OL)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2112  ∀wral 3109   class class class wbr 5033  ‘cfv 6328  (class class class)co 7139  Basecbs 16479  lecple 16568  occoc 16569  joincjn 17550  meetcmee 17551  OLcol 36469  OMLcoml 36470 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rab 3118  df-v 3446  df-un 3889  df-in 3891  df-ss 3901  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-iota 6287  df-fv 6336  df-ov 7142  df-oml 36474 This theorem is referenced by:  omlop  36536  omllat  36537  omllaw3  36540  omllaw4  36541  cmtcomlemN  36543  cmtbr2N  36548  cmtbr3N  36549  omlfh1N  36553  omlfh3N  36554  omlspjN  36556  hlol  36656
 Copyright terms: Public domain W3C validator