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