# Metamath Proof Explorer

## Theorem odujoin

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

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

### Proof

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