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

Metamath Proof Explorer

Theorem isolatiN

Description: Properties that determine an ortholattice. (Contributed by NM, 18-Sep-2011) (New usage is discouraged.)

Ref Expression
Hypotheses isolati.1 ⊢ 𝐾 ∈ Lat
isolati.2 ⊢ 𝐾 ∈ OP
Assertion isolatiN 𝐾 ∈ OL

Proof

Step Hyp Ref Expression
1 isolati.1 ⊢ 𝐾 ∈ Lat
2 isolati.2 ⊢ 𝐾 ∈ OP
3 isolat ⊢ ( 𝐾 ∈ OL ↔ ( 𝐾 ∈ Lat ∧ 𝐾 ∈ OP ) )
4 1 2 3 mpbir2an ⊢ 𝐾 ∈ OL