Nearby theorems
|
|
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > Mathboxes > df-ol | Structured version Visualization version GIF version | ||
| Description: Define the class of ortholattices. Definition from [Kalmbach] p. 16. (Contributed by NM, 18-Sep-2011.) |
| Ref | Expression |
|---|---|
| df-ol | ⊢ OL = (Lat ∩ OP) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | col 39976 | . 2 class OL | |
| 2 | clat 18491 | . . 3 class Lat | |
| 3 | cops 39974 | . . 3 class OP | |
| 4 | 2, 3 | cin 3904 | . 2 class (Lat ∩ OP) |
| 5 | 1, 4 | wceq 1570 | 1 wff OL = (Lat ∩ OP) |
| Colors of variables: wff setvar class |
| This definition is used by: isolat 40014 |
| Copyright terms: Public domain | W3C validator |