# Metamath Proof Explorer

## Theorem oduclatb

Description: Being a complete lattice is self-dual. (Contributed by Stefan O'Rear, 29-Jan-2015)

Ref Expression
Hypothesis oduglb.d ${⊢}{D}=\mathrm{ODual}\left({O}\right)$
Assertion oduclatb ${⊢}{O}\in \mathrm{CLat}↔{D}\in \mathrm{CLat}$

### Proof

Step Hyp Ref Expression
1 oduglb.d ${⊢}{D}=\mathrm{ODual}\left({O}\right)$
2 elex ${⊢}{O}\in \mathrm{CLat}\to {O}\in \mathrm{V}$
3 noel ${⊢}¬\mathrm{lub}\left(\varnothing \right)\left(\varnothing \right)\in \varnothing$
4 ssid ${⊢}\varnothing \subseteq \varnothing$
5 base0 ${⊢}\varnothing ={\mathrm{Base}}_{\varnothing }$
6 eqid ${⊢}\mathrm{lub}\left(\varnothing \right)=\mathrm{lub}\left(\varnothing \right)$
7 5 6 clatlubcl ${⊢}\left(\varnothing \in \mathrm{CLat}\wedge \varnothing \subseteq \varnothing \right)\to \mathrm{lub}\left(\varnothing \right)\left(\varnothing \right)\in \varnothing$
8 4 7 mpan2 ${⊢}\varnothing \in \mathrm{CLat}\to \mathrm{lub}\left(\varnothing \right)\left(\varnothing \right)\in \varnothing$
9 3 8 mto ${⊢}¬\varnothing \in \mathrm{CLat}$
10 fvprc ${⊢}¬{O}\in \mathrm{V}\to \mathrm{ODual}\left({O}\right)=\varnothing$
11 1 10 syl5eq ${⊢}¬{O}\in \mathrm{V}\to {D}=\varnothing$
12 11 eleq1d ${⊢}¬{O}\in \mathrm{V}\to \left({D}\in \mathrm{CLat}↔\varnothing \in \mathrm{CLat}\right)$
13 9 12 mtbiri ${⊢}¬{O}\in \mathrm{V}\to ¬{D}\in \mathrm{CLat}$
14 13 con4i ${⊢}{D}\in \mathrm{CLat}\to {O}\in \mathrm{V}$
15 1 oduposb ${⊢}{O}\in \mathrm{V}\to \left({O}\in \mathrm{Poset}↔{D}\in \mathrm{Poset}\right)$
16 ancom ${⊢}\left(\mathrm{dom}\mathrm{lub}\left({O}\right)=𝒫{\mathrm{Base}}_{{O}}\wedge \mathrm{dom}\mathrm{glb}\left({O}\right)=𝒫{\mathrm{Base}}_{{O}}\right)↔\left(\mathrm{dom}\mathrm{glb}\left({O}\right)=𝒫{\mathrm{Base}}_{{O}}\wedge \mathrm{dom}\mathrm{lub}\left({O}\right)=𝒫{\mathrm{Base}}_{{O}}\right)$
17 eqid ${⊢}\mathrm{glb}\left({O}\right)=\mathrm{glb}\left({O}\right)$
18 1 17 odulub ${⊢}{O}\in \mathrm{V}\to \mathrm{glb}\left({O}\right)=\mathrm{lub}\left({D}\right)$
19 18 dmeqd ${⊢}{O}\in \mathrm{V}\to \mathrm{dom}\mathrm{glb}\left({O}\right)=\mathrm{dom}\mathrm{lub}\left({D}\right)$
20 19 eqeq1d ${⊢}{O}\in \mathrm{V}\to \left(\mathrm{dom}\mathrm{glb}\left({O}\right)=𝒫{\mathrm{Base}}_{{O}}↔\mathrm{dom}\mathrm{lub}\left({D}\right)=𝒫{\mathrm{Base}}_{{O}}\right)$
21 eqid ${⊢}\mathrm{lub}\left({O}\right)=\mathrm{lub}\left({O}\right)$
22 1 21 oduglb ${⊢}{O}\in \mathrm{V}\to \mathrm{lub}\left({O}\right)=\mathrm{glb}\left({D}\right)$
23 22 dmeqd ${⊢}{O}\in \mathrm{V}\to \mathrm{dom}\mathrm{lub}\left({O}\right)=\mathrm{dom}\mathrm{glb}\left({D}\right)$
24 23 eqeq1d ${⊢}{O}\in \mathrm{V}\to \left(\mathrm{dom}\mathrm{lub}\left({O}\right)=𝒫{\mathrm{Base}}_{{O}}↔\mathrm{dom}\mathrm{glb}\left({D}\right)=𝒫{\mathrm{Base}}_{{O}}\right)$
25 20 24 anbi12d ${⊢}{O}\in \mathrm{V}\to \left(\left(\mathrm{dom}\mathrm{glb}\left({O}\right)=𝒫{\mathrm{Base}}_{{O}}\wedge \mathrm{dom}\mathrm{lub}\left({O}\right)=𝒫{\mathrm{Base}}_{{O}}\right)↔\left(\mathrm{dom}\mathrm{lub}\left({D}\right)=𝒫{\mathrm{Base}}_{{O}}\wedge \mathrm{dom}\mathrm{glb}\left({D}\right)=𝒫{\mathrm{Base}}_{{O}}\right)\right)$
26 16 25 syl5bb ${⊢}{O}\in \mathrm{V}\to \left(\left(\mathrm{dom}\mathrm{lub}\left({O}\right)=𝒫{\mathrm{Base}}_{{O}}\wedge \mathrm{dom}\mathrm{glb}\left({O}\right)=𝒫{\mathrm{Base}}_{{O}}\right)↔\left(\mathrm{dom}\mathrm{lub}\left({D}\right)=𝒫{\mathrm{Base}}_{{O}}\wedge \mathrm{dom}\mathrm{glb}\left({D}\right)=𝒫{\mathrm{Base}}_{{O}}\right)\right)$
27 15 26 anbi12d ${⊢}{O}\in \mathrm{V}\to \left(\left({O}\in \mathrm{Poset}\wedge \left(\mathrm{dom}\mathrm{lub}\left({O}\right)=𝒫{\mathrm{Base}}_{{O}}\wedge \mathrm{dom}\mathrm{glb}\left({O}\right)=𝒫{\mathrm{Base}}_{{O}}\right)\right)↔\left({D}\in \mathrm{Poset}\wedge \left(\mathrm{dom}\mathrm{lub}\left({D}\right)=𝒫{\mathrm{Base}}_{{O}}\wedge \mathrm{dom}\mathrm{glb}\left({D}\right)=𝒫{\mathrm{Base}}_{{O}}\right)\right)\right)$
28 eqid ${⊢}{\mathrm{Base}}_{{O}}={\mathrm{Base}}_{{O}}$
29 28 21 17 isclat ${⊢}{O}\in \mathrm{CLat}↔\left({O}\in \mathrm{Poset}\wedge \left(\mathrm{dom}\mathrm{lub}\left({O}\right)=𝒫{\mathrm{Base}}_{{O}}\wedge \mathrm{dom}\mathrm{glb}\left({O}\right)=𝒫{\mathrm{Base}}_{{O}}\right)\right)$
30 1 28 odubas ${⊢}{\mathrm{Base}}_{{O}}={\mathrm{Base}}_{{D}}$
31 eqid ${⊢}\mathrm{lub}\left({D}\right)=\mathrm{lub}\left({D}\right)$
32 eqid ${⊢}\mathrm{glb}\left({D}\right)=\mathrm{glb}\left({D}\right)$
33 30 31 32 isclat ${⊢}{D}\in \mathrm{CLat}↔\left({D}\in \mathrm{Poset}\wedge \left(\mathrm{dom}\mathrm{lub}\left({D}\right)=𝒫{\mathrm{Base}}_{{O}}\wedge \mathrm{dom}\mathrm{glb}\left({D}\right)=𝒫{\mathrm{Base}}_{{O}}\right)\right)$
34 27 29 33 3bitr4g ${⊢}{O}\in \mathrm{V}\to \left({O}\in \mathrm{CLat}↔{D}\in \mathrm{CLat}\right)$
35 2 14 34 pm5.21nii ${⊢}{O}\in \mathrm{CLat}↔{D}\in \mathrm{CLat}$