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 V glb O = lub D
5 4 breqd O V a b glb O c a b lub D c
6 5 oprabbidv O 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 V meet O = a b c | a b glb O c
9 1 fvexi D V
10 eqid lub D = lub D
11 eqid join D = join D
12 10 11 joinfval D V join D = a b c | a b lub D c
13 9 12 mp1i O V join D = a b c | a b lub D c
14 6 8 13 3eqtr4d O V meet O = join D
15 fvprc ¬ O V meet O =
16 fvprc ¬ O V ODual O =
17 1 16 syl5eq ¬ O V D =
18 17 fveq2d ¬ O V join D = join
19 join0 join =
20 18 19 eqtrdi ¬ O V join D =
21 15 20 eqtr4d ¬ O V meet O = join D
22 14 21 pm2.61i meet O = join D
23 2 22 eqtri ˙ = join D