This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = { 𝑙 ∈ 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 ‘ 𝑙 ) ‘ 𝑎 ) ) ) ) }