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 = { 𝑙 ∈ OL ∣ ∀ 𝑎 ∈ ( Base ‘ 𝑙 ) ∀ 𝑏 ∈ ( Base ‘ 𝑙 ) ( 𝑎 ( le ‘ 𝑙 ) 𝑏 → 𝑏 = ( 𝑎 ( join ‘ 𝑙 ) ( 𝑏 ( meet ‘ 𝑙 ) ( ( oc ‘ 𝑙 ) ‘ 𝑎 ) ) ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		coml	⊢ OML
1		vl	⊢ 𝑙
2		col	⊢ OL
3		va	⊢ 𝑎
4		cbs	⊢ Base
5	1	cv	⊢ 𝑙
6	5 4	cfv	⊢ ( Base ‘ 𝑙 )
7		vb	⊢ 𝑏
8	3	cv	⊢ 𝑎
9		cple	⊢ le
10	5 9	cfv	⊢ ( le ‘ 𝑙 )
11	7	cv	⊢ 𝑏
12	8 11 10	wbr	⊢ 𝑎 ( le ‘ 𝑙 ) 𝑏
13		cjn	⊢ join
14	5 13	cfv	⊢ ( join ‘ 𝑙 )
15		cmee	⊢ meet
16	5 15	cfv	⊢ ( meet ‘ 𝑙 )
17		coc	⊢ oc
18	5 17	cfv	⊢ ( oc ‘ 𝑙 )
19	8 18	cfv	⊢ ( ( oc ‘ 𝑙 ) ‘ 𝑎 )
20	11 19 16	co	⊢ ( 𝑏 ( meet ‘ 𝑙 ) ( ( oc ‘ 𝑙 ) ‘ 𝑎 ) )
21	8 20 14	co	⊢ ( 𝑎 ( join ‘ 𝑙 ) ( 𝑏 ( meet ‘ 𝑙 ) ( ( oc ‘ 𝑙 ) ‘ 𝑎 ) ) )
22	11 21	wceq	⊢ 𝑏 = ( 𝑎 ( join ‘ 𝑙 ) ( 𝑏 ( meet ‘ 𝑙 ) ( ( oc ‘ 𝑙 ) ‘ 𝑎 ) ) )
23	12 22	wi	⊢ ( 𝑎 ( le ‘ 𝑙 ) 𝑏 → 𝑏 = ( 𝑎 ( join ‘ 𝑙 ) ( 𝑏 ( meet ‘ 𝑙 ) ( ( oc ‘ 𝑙 ) ‘ 𝑎 ) ) ) )
24	23 7 6	wral	⊢ ∀ 𝑏 ∈ ( Base ‘ 𝑙 ) ( 𝑎 ( le ‘ 𝑙 ) 𝑏 → 𝑏 = ( 𝑎 ( join ‘ 𝑙 ) ( 𝑏 ( meet ‘ 𝑙 ) ( ( oc ‘ 𝑙 ) ‘ 𝑎 ) ) ) )
25	24 3 6	wral	⊢ ∀ 𝑎 ∈ ( Base ‘ 𝑙 ) ∀ 𝑏 ∈ ( Base ‘ 𝑙 ) ( 𝑎 ( le ‘ 𝑙 ) 𝑏 → 𝑏 = ( 𝑎 ( join ‘ 𝑙 ) ( 𝑏 ( meet ‘ 𝑙 ) ( ( oc ‘ 𝑙 ) ‘ 𝑎 ) ) ) )
26	25 1 2	crab	⊢ { 𝑙 ∈ OL ∣ ∀ 𝑎 ∈ ( Base ‘ 𝑙 ) ∀ 𝑏 ∈ ( Base ‘ 𝑙 ) ( 𝑎 ( le ‘ 𝑙 ) 𝑏 → 𝑏 = ( 𝑎 ( join ‘ 𝑙 ) ( 𝑏 ( meet ‘ 𝑙 ) ( ( oc ‘ 𝑙 ) ‘ 𝑎 ) ) ) ) }
27	0 26	wceq	⊢ OML = { 𝑙 ∈ OL ∣ ∀ 𝑎 ∈ ( Base ‘ 𝑙 ) ∀ 𝑏 ∈ ( Base ‘ 𝑙 ) ( 𝑎 ( le ‘ 𝑙 ) 𝑏 → 𝑏 = ( 𝑎 ( join ‘ 𝑙 ) ( 𝑏 ( meet ‘ 𝑙 ) ( ( oc ‘ 𝑙 ) ‘ 𝑎 ) ) ) ) }