| Step |
Hyp |
Ref |
Expression |
| 1 |
|
oduglb.d |
|- D = ( ODual ` O ) |
| 2 |
|
odujoin.m |
|- ./\ = ( meet ` O ) |
| 3 |
|
eqid |
|- ( glb ` O ) = ( glb ` O ) |
| 4 |
1 3
|
odulub |
|- ( O e. _V -> ( glb ` O ) = ( lub ` D ) ) |
| 5 |
4
|
breqd |
|- ( O e. _V -> ( { a , b } ( glb ` O ) c <-> { a , b } ( lub ` D ) c ) ) |
| 6 |
5
|
oprabbidv |
|- ( O e. _V -> { <. <. a , b >. , c >. | { a , b } ( glb ` O ) c } = { <. <. a , b >. , c >. | { a , b } ( lub ` D ) c } ) |
| 7 |
|
eqid |
|- ( meet ` O ) = ( meet ` O ) |
| 8 |
3 7
|
meetfval |
|- ( O e. _V -> ( meet ` O ) = { <. <. a , b >. , c >. | { a , b } ( glb ` O ) c } ) |
| 9 |
1
|
fvexi |
|- D e. _V |
| 10 |
|
eqid |
|- ( lub ` D ) = ( lub ` D ) |
| 11 |
|
eqid |
|- ( join ` D ) = ( join ` D ) |
| 12 |
10 11
|
joinfval |
|- ( D e. _V -> ( join ` D ) = { <. <. a , b >. , c >. | { a , b } ( lub ` D ) c } ) |
| 13 |
9 12
|
mp1i |
|- ( O e. _V -> ( join ` D ) = { <. <. a , b >. , c >. | { a , b } ( lub ` D ) c } ) |
| 14 |
6 8 13
|
3eqtr4d |
|- ( O e. _V -> ( meet ` O ) = ( join ` D ) ) |
| 15 |
|
fvprc |
|- ( -. O e. _V -> ( meet ` O ) = (/) ) |
| 16 |
|
fvprc |
|- ( -. O e. _V -> ( ODual ` O ) = (/) ) |
| 17 |
1 16
|
eqtrid |
|- ( -. O e. _V -> D = (/) ) |
| 18 |
17
|
fveq2d |
|- ( -. O e. _V -> ( join ` D ) = ( join ` (/) ) ) |
| 19 |
|
join0 |
|- ( join ` (/) ) = (/) |
| 20 |
18 19
|
eqtrdi |
|- ( -. O e. _V -> ( join ` D ) = (/) ) |
| 21 |
15 20
|
eqtr4d |
|- ( -. O e. _V -> ( meet ` O ) = ( join ` D ) ) |
| 22 |
14 21
|
pm2.61i |
|- ( meet ` O ) = ( join ` D ) |
| 23 |
2 22
|
eqtri |
|- ./\ = ( join ` D ) |