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 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 )