Theorem omlol 39802

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 2752	. . 3 ⊢ (Base‘𝐾) = (Base‘𝐾)
2		eqid 2752	. . 3 ⊢ (le‘𝐾) = (le‘𝐾)
3		eqid 2752	. . 3 ⊢ (join‘𝐾) = (join‘𝐾)
4		eqid 2752	. . 3 ⊢ (meet‘𝐾) = (meet‘𝐾)
5		eqid 2752	. . 3 ⊢ (oc‘𝐾) = (oc‘𝐾)
6	1, 2, 3, 4, 5	isoml 39800	. 2 ⊢ (𝐾 ∈ OML ↔ (𝐾 ∈ OL ∧ ∀𝑥 ∈ (Base‘𝐾)∀𝑦 ∈ (Base‘𝐾)(𝑥(le‘𝐾)𝑦 → 𝑦 = (𝑥(join‘𝐾)(𝑦(meet‘𝐾)((oc‘𝐾)‘𝑥))))))
7	6	simplbi 499	1 ⊢ (𝐾 ∈ OML → 𝐾 ∈ OL)

Syntax hints:   → wi 4   = wceq 1550   ∈ wcel 2132  ∀wral 3066   class class class wbr 5090  ‘cfv 6506  (class class class)co 7381  Basecbs 17217  lecple 17265  occoc 17266  joincjn 18315  meetcmee 18316  OLcol 39736  OMLcoml 39737

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-ral 3067  df-rab 3405  df-v 3446  df-dif 3898  df-un 3900  df-ss 3912  df-nul 4277  df-if 4471  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-br 5091  df-iota 6462  df-fv 6514  df-ov 7384  df-oml 39741

This theorem is referenced by:  omlop  39803  omllat  39804  omllaw3  39807  omllaw4  39808  cmtcomlemN  39810  cmtbr2N  39815  cmtbr3N  39816  omlfh1N  39820  omlfh3N  39821  omlspjN  39823  hlol  39923