# Metamath Proof Explorer

## Theorem odulatb

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

Ref Expression
Hypothesis oduglb.d ${⊢}{D}=\mathrm{ODual}\left({O}\right)$
Assertion odulatb ${⊢}{O}\in {V}\to \left({O}\in \mathrm{Lat}↔{D}\in \mathrm{Lat}\right)$

### Proof

Step Hyp Ref Expression
1 oduglb.d ${⊢}{D}=\mathrm{ODual}\left({O}\right)$
2 1 oduposb ${⊢}{O}\in {V}\to \left({O}\in \mathrm{Poset}↔{D}\in \mathrm{Poset}\right)$
3 ancom ${⊢}\left(\mathrm{dom}\mathrm{join}\left({O}\right)={\mathrm{Base}}_{{O}}×{\mathrm{Base}}_{{O}}\wedge \mathrm{dom}\mathrm{meet}\left({O}\right)={\mathrm{Base}}_{{O}}×{\mathrm{Base}}_{{O}}\right)↔\left(\mathrm{dom}\mathrm{meet}\left({O}\right)={\mathrm{Base}}_{{O}}×{\mathrm{Base}}_{{O}}\wedge \mathrm{dom}\mathrm{join}\left({O}\right)={\mathrm{Base}}_{{O}}×{\mathrm{Base}}_{{O}}\right)$
4 3 a1i ${⊢}{O}\in {V}\to \left(\left(\mathrm{dom}\mathrm{join}\left({O}\right)={\mathrm{Base}}_{{O}}×{\mathrm{Base}}_{{O}}\wedge \mathrm{dom}\mathrm{meet}\left({O}\right)={\mathrm{Base}}_{{O}}×{\mathrm{Base}}_{{O}}\right)↔\left(\mathrm{dom}\mathrm{meet}\left({O}\right)={\mathrm{Base}}_{{O}}×{\mathrm{Base}}_{{O}}\wedge \mathrm{dom}\mathrm{join}\left({O}\right)={\mathrm{Base}}_{{O}}×{\mathrm{Base}}_{{O}}\right)\right)$
5 2 4 anbi12d ${⊢}{O}\in {V}\to \left(\left({O}\in \mathrm{Poset}\wedge \left(\mathrm{dom}\mathrm{join}\left({O}\right)={\mathrm{Base}}_{{O}}×{\mathrm{Base}}_{{O}}\wedge \mathrm{dom}\mathrm{meet}\left({O}\right)={\mathrm{Base}}_{{O}}×{\mathrm{Base}}_{{O}}\right)\right)↔\left({D}\in \mathrm{Poset}\wedge \left(\mathrm{dom}\mathrm{meet}\left({O}\right)={\mathrm{Base}}_{{O}}×{\mathrm{Base}}_{{O}}\wedge \mathrm{dom}\mathrm{join}\left({O}\right)={\mathrm{Base}}_{{O}}×{\mathrm{Base}}_{{O}}\right)\right)\right)$
6 eqid ${⊢}{\mathrm{Base}}_{{O}}={\mathrm{Base}}_{{O}}$
7 eqid ${⊢}\mathrm{join}\left({O}\right)=\mathrm{join}\left({O}\right)$
8 eqid ${⊢}\mathrm{meet}\left({O}\right)=\mathrm{meet}\left({O}\right)$
9 6 7 8 islat ${⊢}{O}\in \mathrm{Lat}↔\left({O}\in \mathrm{Poset}\wedge \left(\mathrm{dom}\mathrm{join}\left({O}\right)={\mathrm{Base}}_{{O}}×{\mathrm{Base}}_{{O}}\wedge \mathrm{dom}\mathrm{meet}\left({O}\right)={\mathrm{Base}}_{{O}}×{\mathrm{Base}}_{{O}}\right)\right)$
10 1 6 odubas ${⊢}{\mathrm{Base}}_{{O}}={\mathrm{Base}}_{{D}}$
11 1 8 odujoin ${⊢}\mathrm{meet}\left({O}\right)=\mathrm{join}\left({D}\right)$
12 1 7 odumeet ${⊢}\mathrm{join}\left({O}\right)=\mathrm{meet}\left({D}\right)$
13 10 11 12 islat ${⊢}{D}\in \mathrm{Lat}↔\left({D}\in \mathrm{Poset}\wedge \left(\mathrm{dom}\mathrm{meet}\left({O}\right)={\mathrm{Base}}_{{O}}×{\mathrm{Base}}_{{O}}\wedge \mathrm{dom}\mathrm{join}\left({O}\right)={\mathrm{Base}}_{{O}}×{\mathrm{Base}}_{{O}}\right)\right)$
14 5 9 13 3bitr4g ${⊢}{O}\in {V}\to \left({O}\in \mathrm{Lat}↔{D}\in \mathrm{Lat}\right)$