Metamath Proof Explorer

Definition df-oml

Description: Define the class of orthomodular lattices. Definition from Kalmbach p. 16. (Contributed by NM, 18-Sep-2011)

Ref Expression
Assertion 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 ) ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 coml 
 |-  OML
1 vl 
 |-  l
2 col 
 |-  OL
3 va 
 |-  a
4 cbs 
 |-  Base
5 1 cv 
 |-  l
6 5 4 cfv 
 |-  ( Base ` l )
7 vb 
 |-  b
8 3 cv 
 |-  a
9 cple 
 |-  le
10 5 9 cfv 
 |-  ( le ` l )
11 7 cv 
 |-  b
12 8 11 10 wbr 
 |-  a ( le ` l ) b
13 cjn 
 |-  join
14 5 13 cfv 
 |-  ( join ` l )
15 cmee 
 |-  meet
16 5 15 cfv 
 |-  ( meet ` l )
17 coc 
 |-  oc
18 5 17 cfv 
 |-  ( oc ` l )
19 8 18 cfv 
 |-  ( ( oc ` l ) ` a )
20 11 19 16 co 
 |-  ( b ( meet ` l ) ( ( oc ` l ) ` a ) )
21 8 20 14 co 
 |-  ( a ( join ` l ) ( b ( meet ` l ) ( ( oc ` l ) ` a ) ) )
22 11 21 wceq 
 |-  b = ( a ( join ` l ) ( b ( meet ` l ) ( ( oc ` l ) ` a ) ) )
23 12 22 wi 
 |-  ( a ( le ` l ) b -> b = ( a ( join ` l ) ( b ( meet ` l ) ( ( oc ` l ) ` a ) ) ) )
24 23 7 6 wral 
 |-  A. b e. ( Base ` l ) ( a ( le ` l ) b -> b = ( a ( join ` l ) ( b ( meet ` l ) ( ( oc ` l ) ` a ) ) ) )
25 24 3 6 wral 
 |-  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 25 1 2 crab 
 |-  { 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 ) ) ) ) }
27 0 26 wceq 
 |-  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 ) ) ) ) }