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