# Metamath Proof Explorer

## Theorem odumeet

Description: Meets in a dual order are joins in the original. (Contributed by Stefan O'Rear, 29-Jan-2015)

Ref Expression
Hypotheses oduglb.d
`|- D = ( ODual ` O )`
odumeet.j
`|- .\/ = ( join ` O )`
Assertion odumeet
`|- .\/ = ( meet ` D )`

### Proof

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 syl5eq
` |-  ( -. 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 )`