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 )