Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-oml Structured version   Visualization version   GIF version

Definition df-oml 36197
Description: Define the class of orthomodular lattices. Definition from [Kalmbach] p. 16. (Contributed by NM, 18-Sep-2011.)
Assertion
Ref Expression
df-oml OML = {𝑙 ∈ OL ∣ ∀𝑎 ∈ (Base‘𝑙)∀𝑏 ∈ (Base‘𝑙)(𝑎(le‘𝑙)𝑏𝑏 = (𝑎(join‘𝑙)(𝑏(meet‘𝑙)((oc‘𝑙)‘𝑎))))}
Distinct variable group:   𝑎,𝑏,𝑙

Detailed syntax breakdown of Definition df-oml
StepHypRef Expression
1 coml 36193 . 2 class OML
2 va . . . . . . . 8 setvar 𝑎
32cv 1527 . . . . . . 7 class 𝑎
4 vb . . . . . . . 8 setvar 𝑏
54cv 1527 . . . . . . 7 class 𝑏
6 vl . . . . . . . . 9 setvar 𝑙
76cv 1527 . . . . . . . 8 class 𝑙
8 cple 16562 . . . . . . . 8 class le
97, 8cfv 6349 . . . . . . 7 class (le‘𝑙)
103, 5, 9wbr 5058 . . . . . 6 wff 𝑎(le‘𝑙)𝑏
11 coc 16563 . . . . . . . . . . 11 class oc
127, 11cfv 6349 . . . . . . . . . 10 class (oc‘𝑙)
133, 12cfv 6349 . . . . . . . . 9 class ((oc‘𝑙)‘𝑎)
14 cmee 17545 . . . . . . . . . 10 class meet
157, 14cfv 6349 . . . . . . . . 9 class (meet‘𝑙)
165, 13, 15co 7145 . . . . . . . 8 class (𝑏(meet‘𝑙)((oc‘𝑙)‘𝑎))
17 cjn 17544 . . . . . . . . 9 class join
187, 17cfv 6349 . . . . . . . 8 class (join‘𝑙)
193, 16, 18co 7145 . . . . . . 7 class (𝑎(join‘𝑙)(𝑏(meet‘𝑙)((oc‘𝑙)‘𝑎)))
205, 19wceq 1528 . . . . . 6 wff 𝑏 = (𝑎(join‘𝑙)(𝑏(meet‘𝑙)((oc‘𝑙)‘𝑎)))
2110, 20wi 4 . . . . 5 wff (𝑎(le‘𝑙)𝑏𝑏 = (𝑎(join‘𝑙)(𝑏(meet‘𝑙)((oc‘𝑙)‘𝑎))))
22 cbs 16473 . . . . . 6 class Base
237, 22cfv 6349 . . . . 5 class (Base‘𝑙)
2421, 4, 23wral 3138 . . . 4 wff 𝑏 ∈ (Base‘𝑙)(𝑎(le‘𝑙)𝑏𝑏 = (𝑎(join‘𝑙)(𝑏(meet‘𝑙)((oc‘𝑙)‘𝑎))))
2524, 2, 23wral 3138 . . 3 wff 𝑎 ∈ (Base‘𝑙)∀𝑏 ∈ (Base‘𝑙)(𝑎(le‘𝑙)𝑏𝑏 = (𝑎(join‘𝑙)(𝑏(meet‘𝑙)((oc‘𝑙)‘𝑎))))
26 col 36192 . . 3 class OL
2725, 6, 26crab 3142 . 2 class {𝑙 ∈ OL ∣ ∀𝑎 ∈ (Base‘𝑙)∀𝑏 ∈ (Base‘𝑙)(𝑎(le‘𝑙)𝑏𝑏 = (𝑎(join‘𝑙)(𝑏(meet‘𝑙)((oc‘𝑙)‘𝑎))))}
281, 27wceq 1528 1 wff OML = {𝑙 ∈ OL ∣ ∀𝑎 ∈ (Base‘𝑙)∀𝑏 ∈ (Base‘𝑙)(𝑎(le‘𝑙)𝑏𝑏 = (𝑎(join‘𝑙)(𝑏(meet‘𝑙)((oc‘𝑙)‘𝑎))))}
Colors of variables: wff setvar class
This definition is referenced by:  isoml  36256
  Copyright terms: Public domain W3C validator