Definition df-oml 32453

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 32449	. 2 class OML
2		va	. . . . . . . 8 setvar a
3	2	cv 1436	. . . . . . 7 class a
4		vb	. . . . . . . 8 setvar b
5	4	cv 1436	. . . . . . 7 class b
6		vl	. . . . . . . . 9 setvar l
7	6	cv 1436	. . . . . . . 8 class l
8		cple 15159	. . . . . . . 8 class le
9	7, 8	cfv 5601	. . . . . . 7 class ( le ` l )
10	3, 5, 9	wbr 4426	. . . . . 6 wff a ( le ` l ) b
11		coc 15160	. . . . . . . . . . 11 class oc
12	7, 11	cfv 5601	. . . . . . . . . 10 class ( oc ` l )
13	3, 12	cfv 5601	. . . . . . . . 9 class ( ( oc ` l ) ` a )
14		cmee 16141	. . . . . . . . . 10 class meet
15	7, 14	cfv 5601	. . . . . . . . 9 class ( meet ` l )
16	5, 13, 15	co 6305	. . . . . . . 8 class ( b ( meet ` l ) ( ( oc ` l ) ` a ) )
17		cjn 16140	. . . . . . . . 9 class join
18	7, 17	cfv 5601	. . . . . . . 8 class ( join ` l )
19	3, 16, 18	co 6305	. . . . . . 7 class ( a ( join ` l ) ( b ( meet ` l ) ( ( oc ` l ) ` a ) ) )
20	5, 19	wceq 1437	. . . . . 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 15084	. . . . . 6 class Base
23	7, 22	cfv 5601	. . . . 5 class ( Base ` l )
24	21, 4, 23	wral 2782	. . . 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 2782	. . 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 32448	. . 3 class OL
27	25, 6, 26	crab 2786	. 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 1437	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  32512