This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem omlol

Description: An orthomodular lattice is an ortholattice. (Contributed by NM, 18-Sep-2011)

Ref Expression
Assertion omlol ⊢ K ∈ OML → K ∈ OL

Proof

Step Hyp Ref Expression
1 eqid ⊢ Base K = Base K
2 eqid ⊢ ≤ K = ≤ K
3 eqid ⊢ join ⁡ K = join ⁡ K
4 eqid ⊢ meet ⁡ K = meet ⁡ K
5 eqid ⊢ oc ⁡ K = oc ⁡ K
6 1 2 3 4 5 isoml ⊢ K ∈ OML ↔ K ∈ OL ∧ ∀ x ∈ Base K ∀ y ∈ Base K x ≤ K y → y = x join ⁡ K y meet ⁡ K oc ⁡ K ⁡ x
7 6 simplbi ⊢ K ∈ OML → K ∈ OL