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 ∈ OL | ∀ a ∈ Base l ∀ b ∈ Base l a ≤ l b → b = a join ⁡ l b meet ⁡ l oc ⁡ l ⁡ a

Detailed syntax breakdown

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 ≤ l
11 7 cv setvar b
12 8 11 10 wbr wff a ≤ 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 ≤ l b → b = a join ⁡ l b meet ⁡ l oc ⁡ l ⁡ a
24 23 7 6 wral wff ∀ b ∈ Base l a ≤ l b → b = a join ⁡ l b meet ⁡ l oc ⁡ l ⁡ a
25 24 3 6 wral wff ∀ a ∈ Base l ∀ b ∈ Base l a ≤ l b → b = a join ⁡ l b meet ⁡ l oc ⁡ l ⁡ a
26 25 1 2 crab class l ∈ OL | ∀ a ∈ Base l ∀ b ∈ Base l a ≤ l b → b = a join ⁡ l b meet ⁡ l oc ⁡ l ⁡ a
27 0 26 wceq wff OML = l ∈ OL | ∀ a ∈ Base l ∀ b ∈ Base l a ≤ l b → b = a join ⁡ l b meet ⁡ l oc ⁡ l ⁡ a