# Metamath Proof Explorer

## Theorem odulub

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

Ref Expression
Hypotheses oduglb.d ${⊢}{D}=\mathrm{ODual}\left({O}\right)$
odulub.l ${⊢}{L}=\mathrm{glb}\left({O}\right)$
Assertion odulub ${⊢}{O}\in {V}\to {L}=\mathrm{lub}\left({D}\right)$

### Proof

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