Theorem omlol 39869

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.

Step	Hyp	Ref	Expression
1		eqid 2763	. . 3 ⊢ (Base‘𝐾) = (Base‘𝐾)
2		eqid 2763	. . 3 ⊢ (le‘𝐾) = (le‘𝐾)
3		eqid 2763	. . 3 ⊢ (join‘𝐾) = (join‘𝐾)
4		eqid 2763	. . 3 ⊢ (meet‘𝐾) = (meet‘𝐾)
5		eqid 2763	. . 3 ⊢ (oc‘𝐾) = (oc‘𝐾)
6	1, 2, 3, 4, 5	isoml 39867	. 2 ⊢ (𝐾 ∈ OML ↔ (𝐾 ∈ OL ∧ ∀𝑥 ∈ (Base‘𝐾)∀𝑦 ∈ (Base‘𝐾)(𝑥(le‘𝐾)𝑦 → 𝑦 = (𝑥(join‘𝐾)(𝑦(meet‘𝐾)((oc‘𝐾)‘𝑥))))))
7	6	simplbi 500	1 ⊢ (𝐾 ∈ OML → 𝐾 ∈ OL)

Syntax hints:   → wi 4   = wceq 1561   ∈ wcel 2143  ∀wral 3077   class class class wbr 5101  ‘cfv 6521  (class class class)co 7396  Basecbs 17255  lecple 17303  occoc 17304  joincjn 18353  meetcmee 18354  OLcol 39803  OMLcoml 39804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3078  df-rab 3416  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5102  df-iota 6477  df-fv 6529  df-ov 7399  df-oml 39808

This theorem is referenced by:  omlop  39870  omllat  39871  omllaw3  39874  omllaw4  39875  cmtcomlemN  39877  cmtbr2N  39882  cmtbr3N  39883  omlfh1N  39887  omlfh3N  39888  omlspjN  39890  hlol  39990