# 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}=\mathrm{ODual}\left({O}\right)$
oduglb.l ${⊢}{U}=\mathrm{lub}\left({O}\right)$
Assertion oduglb ${⊢}{O}\in {V}\to {U}=\mathrm{glb}\left({D}\right)$

### Proof

Step Hyp Ref Expression
1 oduglb.d ${⊢}{D}=\mathrm{ODual}\left({O}\right)$
2 oduglb.l ${⊢}{U}=\mathrm{lub}\left({O}\right)$
3 vex ${⊢}{b}\in \mathrm{V}$
4 vex ${⊢}{c}\in \mathrm{V}$
5 3 4 brcnv ${⊢}{b}{{\le }_{{O}}}^{-1}{c}↔{c}{\le }_{{O}}{b}$
6 5 ralbii ${⊢}\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{b}{{\le }_{{O}}}^{-1}{c}↔\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}{\le }_{{O}}{b}$
7 vex ${⊢}{d}\in \mathrm{V}$
8 7 4 brcnv ${⊢}{d}{{\le }_{{O}}}^{-1}{c}↔{c}{\le }_{{O}}{d}$
9 8 ralbii ${⊢}\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{d}{{\le }_{{O}}}^{-1}{c}↔\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}{\le }_{{O}}{d}$
10 7 3 brcnv ${⊢}{d}{{\le }_{{O}}}^{-1}{b}↔{b}{\le }_{{O}}{d}$
11 9 10 imbi12i ${⊢}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{d}{{\le }_{{O}}}^{-1}{c}\to {d}{{\le }_{{O}}}^{-1}{b}\right)↔\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}{\le }_{{O}}{d}\to {b}{\le }_{{O}}{d}\right)$
12 11 ralbii ${⊢}\forall {d}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{d}{{\le }_{{O}}}^{-1}{c}\to {d}{{\le }_{{O}}}^{-1}{b}\right)↔\forall {d}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}{\le }_{{O}}{d}\to {b}{\le }_{{O}}{d}\right)$
13 6 12 anbi12i ${⊢}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{b}{{\le }_{{O}}}^{-1}{c}\wedge \forall {d}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{d}{{\le }_{{O}}}^{-1}{c}\to {d}{{\le }_{{O}}}^{-1}{b}\right)\right)↔\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}{\le }_{{O}}{b}\wedge \forall {d}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}{\le }_{{O}}{d}\to {b}{\le }_{{O}}{d}\right)\right)$
14 13 a1i ${⊢}{b}\in {\mathrm{Base}}_{{O}}\to \left(\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{b}{{\le }_{{O}}}^{-1}{c}\wedge \forall {d}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{d}{{\le }_{{O}}}^{-1}{c}\to {d}{{\le }_{{O}}}^{-1}{b}\right)\right)↔\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}{\le }_{{O}}{b}\wedge \forall {d}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}{\le }_{{O}}{d}\to {b}{\le }_{{O}}{d}\right)\right)\right)$
15 14 riotabiia ${⊢}\left(\iota {b}\in {\mathrm{Base}}_{{O}}|\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{b}{{\le }_{{O}}}^{-1}{c}\wedge \forall {d}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{d}{{\le }_{{O}}}^{-1}{c}\to {d}{{\le }_{{O}}}^{-1}{b}\right)\right)\right)=\left(\iota {b}\in {\mathrm{Base}}_{{O}}|\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}{\le }_{{O}}{b}\wedge \forall {d}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}{\le }_{{O}}{d}\to {b}{\le }_{{O}}{d}\right)\right)\right)$
16 15 mpteq2i ${⊢}\left({a}\in 𝒫{\mathrm{Base}}_{{O}}⟼\left(\iota {b}\in {\mathrm{Base}}_{{O}}|\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{b}{{\le }_{{O}}}^{-1}{c}\wedge \forall {d}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{d}{{\le }_{{O}}}^{-1}{c}\to {d}{{\le }_{{O}}}^{-1}{b}\right)\right)\right)\right)=\left({a}\in 𝒫{\mathrm{Base}}_{{O}}⟼\left(\iota {b}\in {\mathrm{Base}}_{{O}}|\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}{\le }_{{O}}{b}\wedge \forall {d}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}{\le }_{{O}}{d}\to {b}{\le }_{{O}}{d}\right)\right)\right)\right)$
17 13 reubii ${⊢}\exists !{b}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{b}{{\le }_{{O}}}^{-1}{c}\wedge \forall {d}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{d}{{\le }_{{O}}}^{-1}{c}\to {d}{{\le }_{{O}}}^{-1}{b}\right)\right)↔\exists !{b}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}{\le }_{{O}}{b}\wedge \forall {d}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}{\le }_{{O}}{d}\to {b}{\le }_{{O}}{d}\right)\right)$
18 17 abbii ${⊢}\left\{{a}|\exists !{b}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{b}{{\le }_{{O}}}^{-1}{c}\wedge \forall {d}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{d}{{\le }_{{O}}}^{-1}{c}\to {d}{{\le }_{{O}}}^{-1}{b}\right)\right)\right\}=\left\{{a}|\exists !{b}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}{\le }_{{O}}{b}\wedge \forall {d}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}{\le }_{{O}}{d}\to {b}{\le }_{{O}}{d}\right)\right)\right\}$
19 16 18 reseq12i ${⊢}{\left({a}\in 𝒫{\mathrm{Base}}_{{O}}⟼\left(\iota {b}\in {\mathrm{Base}}_{{O}}|\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{b}{{\le }_{{O}}}^{-1}{c}\wedge \forall {d}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{d}{{\le }_{{O}}}^{-1}{c}\to {d}{{\le }_{{O}}}^{-1}{b}\right)\right)\right)\right)↾}_{\left\{{a}|\exists !{b}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{b}{{\le }_{{O}}}^{-1}{c}\wedge \forall {d}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{d}{{\le }_{{O}}}^{-1}{c}\to {d}{{\le }_{{O}}}^{-1}{b}\right)\right)\right\}}={\left({a}\in 𝒫{\mathrm{Base}}_{{O}}⟼\left(\iota {b}\in {\mathrm{Base}}_{{O}}|\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}{\le }_{{O}}{b}\wedge \forall {d}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}{\le }_{{O}}{d}\to {b}{\le }_{{O}}{d}\right)\right)\right)\right)↾}_{\left\{{a}|\exists !{b}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}{\le }_{{O}}{b}\wedge \forall {d}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}{\le }_{{O}}{d}\to {b}{\le }_{{O}}{d}\right)\right)\right\}}$
20 19 eqcomi ${⊢}{\left({a}\in 𝒫{\mathrm{Base}}_{{O}}⟼\left(\iota {b}\in {\mathrm{Base}}_{{O}}|\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}{\le }_{{O}}{b}\wedge \forall {d}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}{\le }_{{O}}{d}\to {b}{\le }_{{O}}{d}\right)\right)\right)\right)↾}_{\left\{{a}|\exists !{b}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}{\le }_{{O}}{b}\wedge \forall {d}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}{\le }_{{O}}{d}\to {b}{\le }_{{O}}{d}\right)\right)\right\}}={\left({a}\in 𝒫{\mathrm{Base}}_{{O}}⟼\left(\iota {b}\in {\mathrm{Base}}_{{O}}|\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{b}{{\le }_{{O}}}^{-1}{c}\wedge \forall {d}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{d}{{\le }_{{O}}}^{-1}{c}\to {d}{{\le }_{{O}}}^{-1}{b}\right)\right)\right)\right)↾}_{\left\{{a}|\exists !{b}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{b}{{\le }_{{O}}}^{-1}{c}\wedge \forall {d}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{d}{{\le }_{{O}}}^{-1}{c}\to {d}{{\le }_{{O}}}^{-1}{b}\right)\right)\right\}}$
21 eqid ${⊢}{\mathrm{Base}}_{{O}}={\mathrm{Base}}_{{O}}$
22 eqid ${⊢}{\le }_{{O}}={\le }_{{O}}$
23 eqid ${⊢}\mathrm{lub}\left({O}\right)=\mathrm{lub}\left({O}\right)$
24 biid ${⊢}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}{\le }_{{O}}{b}\wedge \forall {d}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}{\le }_{{O}}{d}\to {b}{\le }_{{O}}{d}\right)\right)↔\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}{\le }_{{O}}{b}\wedge \forall {d}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}{\le }_{{O}}{d}\to {b}{\le }_{{O}}{d}\right)\right)$
25 id ${⊢}{O}\in {V}\to {O}\in {V}$
26 21 22 23 24 25 lubfval ${⊢}{O}\in {V}\to \mathrm{lub}\left({O}\right)={\left({a}\in 𝒫{\mathrm{Base}}_{{O}}⟼\left(\iota {b}\in {\mathrm{Base}}_{{O}}|\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}{\le }_{{O}}{b}\wedge \forall {d}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}{\le }_{{O}}{d}\to {b}{\le }_{{O}}{d}\right)\right)\right)\right)↾}_{\left\{{a}|\exists !{b}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}{\le }_{{O}}{b}\wedge \forall {d}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}{\le }_{{O}}{d}\to {b}{\le }_{{O}}{d}\right)\right)\right\}}$
27 1 fvexi ${⊢}{D}\in \mathrm{V}$
28 1 21 odubas ${⊢}{\mathrm{Base}}_{{O}}={\mathrm{Base}}_{{D}}$
29 1 22 oduleval ${⊢}{{\le }_{{O}}}^{-1}={\le }_{{D}}$
30 eqid ${⊢}\mathrm{glb}\left({D}\right)=\mathrm{glb}\left({D}\right)$
31 biid ${⊢}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{b}{{\le }_{{O}}}^{-1}{c}\wedge \forall {d}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{d}{{\le }_{{O}}}^{-1}{c}\to {d}{{\le }_{{O}}}^{-1}{b}\right)\right)↔\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{b}{{\le }_{{O}}}^{-1}{c}\wedge \forall {d}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{d}{{\le }_{{O}}}^{-1}{c}\to {d}{{\le }_{{O}}}^{-1}{b}\right)\right)$
32 id ${⊢}{D}\in \mathrm{V}\to {D}\in \mathrm{V}$
33 28 29 30 31 32 glbfval ${⊢}{D}\in \mathrm{V}\to \mathrm{glb}\left({D}\right)={\left({a}\in 𝒫{\mathrm{Base}}_{{O}}⟼\left(\iota {b}\in {\mathrm{Base}}_{{O}}|\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{b}{{\le }_{{O}}}^{-1}{c}\wedge \forall {d}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{d}{{\le }_{{O}}}^{-1}{c}\to {d}{{\le }_{{O}}}^{-1}{b}\right)\right)\right)\right)↾}_{\left\{{a}|\exists !{b}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{b}{{\le }_{{O}}}^{-1}{c}\wedge \forall {d}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{d}{{\le }_{{O}}}^{-1}{c}\to {d}{{\le }_{{O}}}^{-1}{b}\right)\right)\right\}}$
34 27 33 mp1i ${⊢}{O}\in {V}\to \mathrm{glb}\left({D}\right)={\left({a}\in 𝒫{\mathrm{Base}}_{{O}}⟼\left(\iota {b}\in {\mathrm{Base}}_{{O}}|\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{b}{{\le }_{{O}}}^{-1}{c}\wedge \forall {d}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{d}{{\le }_{{O}}}^{-1}{c}\to {d}{{\le }_{{O}}}^{-1}{b}\right)\right)\right)\right)↾}_{\left\{{a}|\exists !{b}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{b}{{\le }_{{O}}}^{-1}{c}\wedge \forall {d}\in {\mathrm{Base}}_{{O}}\phantom{\rule{.4em}{0ex}}\left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{d}{{\le }_{{O}}}^{-1}{c}\to {d}{{\le }_{{O}}}^{-1}{b}\right)\right)\right\}}$
35 20 26 34 3eqtr4a ${⊢}{O}\in {V}\to \mathrm{lub}\left({O}\right)=\mathrm{glb}\left({D}\right)$
36 2 35 syl5eq ${⊢}{O}\in {V}\to {U}=\mathrm{glb}\left({D}\right)$