Theorem omlol 39729

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

Syntax hints:   → wi 4   = wceq 1543   ∈ wcel 2115  ∀wral 3050   class class class wbr 5075  ‘cfv 6488  (class class class)co 7359  Basecbs 17173  lecple 17221  occoc 17222  joincjn 18271  meetcmee 18272  OLcol 39663  OMLcoml 39664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1970  ax-7 2011  ax-8 2117  ax-9 2125  ax-ext 2708

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 850  df-3an 1090  df-tru 1546  df-fal 1556  df-ex 1783  df-sb 2070  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3051  df-rab 3389  df-v 3430  df-dif 3889  df-un 3891  df-ss 3903  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-iota 6444  df-fv 6496  df-ov 7362  df-oml 39668

This theorem is referenced by:  omlop  39730  omllat  39731  omllaw3  39734  omllaw4  39735  cmtcomlemN  39737  cmtbr2N  39742  cmtbr3N  39743  omlfh1N  39747  omlfh3N  39748  omlspjN  39750  hlol  39850