Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-oml Unicode version

Definition df-oml 29369
Description: Define the class of orthomodular lattices. Definition from [Kalmbach] p. 16. (Contributed by NM, 18-Sep-2011.)
Assertion
Ref Expression
df-oml  |-  OML  =  { l  e.  OL  |  A. a  e.  (
Base `  l ) A. b  e.  ( Base `  l ) ( a ( le `  l ) b  -> 
b  =  ( a ( join `  l
) ( b (
meet `  l )
( ( oc `  l ) `  a
) ) ) ) }
Distinct variable group:    a, b, l

Detailed syntax breakdown of Definition df-oml
StepHypRef Expression
1 coml 29365 . 2  class  OML
2 va . . . . . . . 8  set  a
32cv 1622 . . . . . . 7  class  a
4 vb . . . . . . . 8  set  b
54cv 1622 . . . . . . 7  class  b
6 vl . . . . . . . . 9  set  l
76cv 1622 . . . . . . . 8  class  l
8 cple 13215 . . . . . . . 8  class  le
97, 8cfv 5255 . . . . . . 7  class  ( le
`  l )
103, 5, 9wbr 4023 . . . . . 6  wff  a ( le `  l ) b
11 coc 13216 . . . . . . . . . . 11  class  oc
127, 11cfv 5255 . . . . . . . . . 10  class  ( oc
`  l )
133, 12cfv 5255 . . . . . . . . 9  class  ( ( oc `  l ) `
 a )
14 cmee 14079 . . . . . . . . . 10  class  meet
157, 14cfv 5255 . . . . . . . . 9  class  ( meet `  l )
165, 13, 15co 5858 . . . . . . . 8  class  ( b ( meet `  l
) ( ( oc
`  l ) `  a ) )
17 cjn 14078 . . . . . . . . 9  class  join
187, 17cfv 5255 . . . . . . . 8  class  ( join `  l )
193, 16, 18co 5858 . . . . . . 7  class  ( a ( join `  l
) ( b (
meet `  l )
( ( oc `  l ) `  a
) ) )
205, 19wceq 1623 . . . . . 6  wff  b  =  ( a ( join `  l ) ( b ( meet `  l
) ( ( oc
`  l ) `  a ) ) )
2110, 20wi 4 . . . . 5  wff  ( a ( le `  l
) b  ->  b  =  ( a (
join `  l )
( b ( meet `  l ) ( ( oc `  l ) `
 a ) ) ) )
22 cbs 13148 . . . . . 6  class  Base
237, 22cfv 5255 . . . . 5  class  ( Base `  l )
2421, 4, 23wral 2543 . . . 4  wff  A. b  e.  ( Base `  l
) ( a ( le `  l ) b  ->  b  =  ( a ( join `  l ) ( b ( meet `  l
) ( ( oc
`  l ) `  a ) ) ) )
2524, 2, 23wral 2543 . . 3  wff  A. a  e.  ( Base `  l
) A. b  e.  ( Base `  l
) ( a ( le `  l ) b  ->  b  =  ( a ( join `  l ) ( b ( meet `  l
) ( ( oc
`  l ) `  a ) ) ) )
26 col 29364 . . 3  class  OL
2725, 6, 26crab 2547 . 2  class  { l  e.  OL  |  A. a  e.  ( Base `  l ) A. b  e.  ( Base `  l
) ( a ( le `  l ) b  ->  b  =  ( a ( join `  l ) ( b ( meet `  l
) ( ( oc
`  l ) `  a ) ) ) ) }
281, 27wceq 1623 1  wff  OML  =  { l  e.  OL  |  A. a  e.  (
Base `  l ) A. b  e.  ( Base `  l ) ( a ( le `  l ) b  -> 
b  =  ( a ( join `  l
) ( b (
meet `  l )
( ( oc `  l ) `  a
) ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  isoml  29428
  Copyright terms: Public domain W3C validator