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