Definition df-oml 39180

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

Step	Hyp	Ref	Expression
1		coml 39176	. 2 class OML
2		va	. . . . . . . 8 setvar 𝑎
3	2	cv 1539	. . . . . . 7 class 𝑎
4		vb	. . . . . . . 8 setvar 𝑏
5	4	cv 1539	. . . . . . 7 class 𝑏
6		vl	. . . . . . . . 9 setvar 𝑙
7	6	cv 1539	. . . . . . . 8 class 𝑙
8		cple 17304	. . . . . . . 8 class le
9	7, 8	cfv 6561	. . . . . . 7 class (le‘𝑙)
10	3, 5, 9	wbr 5143	. . . . . 6 wff 𝑎(le‘𝑙)𝑏
11		coc 17305	. . . . . . . . . . 11 class oc
12	7, 11	cfv 6561	. . . . . . . . . 10 class (oc‘𝑙)
13	3, 12	cfv 6561	. . . . . . . . 9 class ((oc‘𝑙)‘𝑎)
14		cmee 18358	. . . . . . . . . 10 class meet
15	7, 14	cfv 6561	. . . . . . . . 9 class (meet‘𝑙)
16	5, 13, 15	co 7431	. . . . . . . 8 class (𝑏(meet‘𝑙)((oc‘𝑙)‘𝑎))
17		cjn 18357	. . . . . . . . 9 class join
18	7, 17	cfv 6561	. . . . . . . 8 class (join‘𝑙)
19	3, 16, 18	co 7431	. . . . . . 7 class (𝑎(join‘𝑙)(𝑏(meet‘𝑙)((oc‘𝑙)‘𝑎)))
20	5, 19	wceq 1540	. . . . . 6 wff 𝑏 = (𝑎(join‘𝑙)(𝑏(meet‘𝑙)((oc‘𝑙)‘𝑎)))
21	10, 20	wi 4	. . . . 5 wff (𝑎(le‘𝑙)𝑏 → 𝑏 = (𝑎(join‘𝑙)(𝑏(meet‘𝑙)((oc‘𝑙)‘𝑎))))
22		cbs 17247	. . . . . 6 class Base
23	7, 22	cfv 6561	. . . . 5 class (Base‘𝑙)
24	21, 4, 23	wral 3061	. . . 4 wff ∀𝑏 ∈ (Base‘𝑙)(𝑎(le‘𝑙)𝑏 → 𝑏 = (𝑎(join‘𝑙)(𝑏(meet‘𝑙)((oc‘𝑙)‘𝑎))))
25	24, 2, 23	wral 3061	. . 3 wff ∀𝑎 ∈ (Base‘𝑙)∀𝑏 ∈ (Base‘𝑙)(𝑎(le‘𝑙)𝑏 → 𝑏 = (𝑎(join‘𝑙)(𝑏(meet‘𝑙)((oc‘𝑙)‘𝑎))))
26		col 39175	. . 3 class OL
27	25, 6, 26	crab 3436	. 2 class {𝑙 ∈ OL ∣ ∀𝑎 ∈ (Base‘𝑙)∀𝑏 ∈ (Base‘𝑙)(𝑎(le‘𝑙)𝑏 → 𝑏 = (𝑎(join‘𝑙)(𝑏(meet‘𝑙)((oc‘𝑙)‘𝑎))))}
28	1, 27	wceq 1540	1 wff OML = {𝑙 ∈ OL ∣ ∀𝑎 ∈ (Base‘𝑙)∀𝑏 ∈ (Base‘𝑙)(𝑎(le‘𝑙)𝑏 → 𝑏 = (𝑎(join‘𝑙)(𝑏(meet‘𝑙)((oc‘𝑙)‘𝑎))))}

This definition is referenced by:  isoml  39239