Definition df-oml 34779

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

Step	Hyp	Ref	Expression
1		coml 34775	. 2 class OML
2		va	. . . . . . . 8 setvar a
3	2	cv 1382	. . . . . . 7 class a
4		vb	. . . . . . . 8 setvar b
5	4	cv 1382	. . . . . . 7 class b
6		vl	. . . . . . . . 9 setvar l
7	6	cv 1382	. . . . . . . 8 class l
8		cple 14686	. . . . . . . 8 class le
9	7, 8	cfv 5578	. . . . . . 7 class ( le ` l )
10	3, 5, 9	wbr 4437	. . . . . 6 wff a ( le ` l ) b
11		coc 14687	. . . . . . . . . . 11 class oc
12	7, 11	cfv 5578	. . . . . . . . . 10 class ( oc ` l )
13	3, 12	cfv 5578	. . . . . . . . 9 class ( ( oc ` l ) ` a )
14		cmee 15553	. . . . . . . . . 10 class meet
15	7, 14	cfv 5578	. . . . . . . . 9 class ( meet ` l )
16	5, 13, 15	co 6281	. . . . . . . 8 class ( b ( meet ` l ) ( ( oc ` l ) ` a ) )
17		cjn 15552	. . . . . . . . 9 class join
18	7, 17	cfv 5578	. . . . . . . 8 class ( join ` l )
19	3, 16, 18	co 6281	. . . . . . 7 class ( a ( join ` l ) ( b ( meet ` l ) ( ( oc ` l ) ` a ) ) )
20	5, 19	wceq 1383	. . . . . 6 wff b = ( a ( join ` l ) ( b ( meet ` l ) ( ( oc ` l ) ` a ) ) )
21	10, 20	wi 4	. . . . 5 wff ( a ( le ` l ) b -> b = ( a ( join ` l ) ( b ( meet ` l ) ( ( oc ` l ) ` a ) ) ) )
22		cbs 14614	. . . . . 6 class Base
23	7, 22	cfv 5578	. . . . 5 class ( Base ` l )
24	21, 4, 23	wral 2793	. . . 4 wff A. b e. ( Base ` l ) ( a ( le ` l ) b -> b = ( a ( join ` l ) ( b ( meet ` l ) ( ( oc ` l ) ` a ) ) ) )
25	24, 2, 23	wral 2793	. . 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 34774	. . 3 class OL
27	25, 6, 26	crab 2797	. 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 ) ) ) ) }
28	1, 27	wceq 1383	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 ) ) ) ) }

This definition is referenced by:  isoml  34838