Metamath Proof Explorer


Theorem oduglb

Description: Greatest lower bounds in a dual order are least upper bounds in the original order. (Contributed by Stefan O'Rear, 29-Jan-2015)

Ref Expression
Hypotheses oduglb.d D = ODual O
oduglb.l U = lub O
Assertion oduglb O V U = glb D

Proof

Step Hyp Ref Expression
1 oduglb.d D = ODual O
2 oduglb.l U = lub O
3 vex b V
4 vex c V
5 3 4 brcnv b O -1 c c O b
6 5 ralbii c a b O -1 c c a c O b
7 vex d V
8 7 4 brcnv d O -1 c c O d
9 8 ralbii c a d O -1 c c a c O d
10 7 3 brcnv d O -1 b b O d
11 9 10 imbi12i c a d O -1 c d O -1 b c a c O d b O d
12 11 ralbii d Base O c a d O -1 c d O -1 b d Base O c a c O d b O d
13 6 12 anbi12i c a b O -1 c d Base O c a d O -1 c d O -1 b c a c O b d Base O c a c O d b O d
14 13 a1i b Base O c a b O -1 c d Base O c a d O -1 c d O -1 b c a c O b d Base O c a c O d b O d
15 14 riotabiia ι b Base O | c a b O -1 c d Base O c a d O -1 c d O -1 b = ι b Base O | c a c O b d Base O c a c O d b O d
16 15 mpteq2i a 𝒫 Base O ι b Base O | c a b O -1 c d Base O c a d O -1 c d O -1 b = a 𝒫 Base O ι b Base O | c a c O b d Base O c a c O d b O d
17 13 reubii ∃! b Base O c a b O -1 c d Base O c a d O -1 c d O -1 b ∃! b Base O c a c O b d Base O c a c O d b O d
18 17 abbii a | ∃! b Base O c a b O -1 c d Base O c a d O -1 c d O -1 b = a | ∃! b Base O c a c O b d Base O c a c O d b O d
19 16 18 reseq12i a 𝒫 Base O ι b Base O | c a b O -1 c d Base O c a d O -1 c d O -1 b a | ∃! b Base O c a b O -1 c d Base O c a d O -1 c d O -1 b = a 𝒫 Base O ι b Base O | c a c O b d Base O c a c O d b O d a | ∃! b Base O c a c O b d Base O c a c O d b O d
20 19 eqcomi a 𝒫 Base O ι b Base O | c a c O b d Base O c a c O d b O d a | ∃! b Base O c a c O b d Base O c a c O d b O d = a 𝒫 Base O ι b Base O | c a b O -1 c d Base O c a d O -1 c d O -1 b a | ∃! b Base O c a b O -1 c d Base O c a d O -1 c d O -1 b
21 eqid Base O = Base O
22 eqid O = O
23 eqid lub O = lub O
24 biid c a c O b d Base O c a c O d b O d c a c O b d Base O c a c O d b O d
25 id O V O V
26 21 22 23 24 25 lubfval O V lub O = a 𝒫 Base O ι b Base O | c a c O b d Base O c a c O d b O d a | ∃! b Base O c a c O b d Base O c a c O d b O d
27 1 fvexi D V
28 1 21 odubas Base O = Base D
29 1 22 oduleval O -1 = D
30 eqid glb D = glb D
31 biid c a b O -1 c d Base O c a d O -1 c d O -1 b c a b O -1 c d Base O c a d O -1 c d O -1 b
32 id D V D V
33 28 29 30 31 32 glbfval D V glb D = a 𝒫 Base O ι b Base O | c a b O -1 c d Base O c a d O -1 c d O -1 b a | ∃! b Base O c a b O -1 c d Base O c a d O -1 c d O -1 b
34 27 33 mp1i O V glb D = a 𝒫 Base O ι b Base O | c a b O -1 c d Base O c a d O -1 c d O -1 b a | ∃! b Base O c a b O -1 c d Base O c a d O -1 c d O -1 b
35 20 26 34 3eqtr4a O V lub O = glb D
36 2 35 syl5eq O V U = glb D