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 \in OL \| \forall a \in {Base}_{l} \forall b \in {Base}_{l} (a \leq_{l} b \to b = a join (l) (b meet (l) oc (l) (a)))\}$

Step	Hyp	Ref	Expression
0		coml	$class OML$
1		vl	$setvar l$
2		col	$class OL$
3		va	$setvar a$
4		cbs	$class Base$
5	1	cv	$setvar l$
6	5 4	cfv	$class {Base}_{l}$
7		vb	$setvar b$
8	3	cv	$setvar a$
9		cple	$class le$
10	5 9	cfv	$class \leq_{l}$
11	7	cv	$setvar b$
12	8 11 10	wbr	$wff a \leq_{l} b$
13		cjn	$class join$
14	5 13	cfv	$class join (l)$
15		cmee	$class meet$
16	5 15	cfv	$class meet (l)$
17		coc	$class oc$
18	5 17	cfv	$class oc (l)$
19	8 18	cfv	$class oc (l) (a)$
20	11 19 16	co	$class (b meet (l) oc (l) (a))$
21	8 20 14	co	$class (a join (l) (b meet (l) oc (l) (a)))$
22	11 21	wceq	$wff b = a join (l) (b meet (l) oc (l) (a))$
23	12 22	wi	$wff (a \leq_{l} b \to b = a join (l) (b meet (l) oc (l) (a)))$
24	23 7 6	wral	$wff \forall b \in {Base}_{l} (a \leq_{l} b \to b = a join (l) (b meet (l) oc (l) (a)))$
25	24 3 6	wral	$wff \forall a \in {Base}_{l} \forall b \in {Base}_{l} (a \leq_{l} b \to b = a join (l) (b meet (l) oc (l) (a)))$
26	25 1 2	crab	$class \{l \in OL \| \forall a \in {Base}_{l} \forall b \in {Base}_{l} (a \leq_{l} b \to b = a join (l) (b meet (l) oc (l) (a)))\}$
27	0 26	wceq	$wff OML = \{l \in OL \| \forall a \in {Base}_{l} \forall b \in {Base}_{l} (a \leq_{l} b \to b = a join (l) (b meet (l) oc (l) (a)))\}$

Metamath Proof Explorer