# 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 = ( ODual ` O )`
Assertion odulatb
`|- ( O e. V -> ( O e. Lat <-> D e. Lat ) )`

### Proof

Step Hyp Ref Expression
1 oduglb.d
` |-  D = ( ODual ` O )`
2 1 oduposb
` |-  ( O e. V -> ( O e. Poset <-> D e. Poset ) )`
3 ancom
` |-  ( ( dom ( join ` O ) = ( ( Base ` O ) X. ( Base ` O ) ) /\ dom ( meet ` O ) = ( ( Base ` O ) X. ( Base ` O ) ) ) <-> ( dom ( meet ` O ) = ( ( Base ` O ) X. ( Base ` O ) ) /\ dom ( join ` O ) = ( ( Base ` O ) X. ( Base ` O ) ) ) )`
4 3 a1i
` |-  ( O e. V -> ( ( dom ( join ` O ) = ( ( Base ` O ) X. ( Base ` O ) ) /\ dom ( meet ` O ) = ( ( Base ` O ) X. ( Base ` O ) ) ) <-> ( dom ( meet ` O ) = ( ( Base ` O ) X. ( Base ` O ) ) /\ dom ( join ` O ) = ( ( Base ` O ) X. ( Base ` O ) ) ) ) )`
5 2 4 anbi12d
` |-  ( O e. V -> ( ( O e. Poset /\ ( dom ( join ` O ) = ( ( Base ` O ) X. ( Base ` O ) ) /\ dom ( meet ` O ) = ( ( Base ` O ) X. ( Base ` O ) ) ) ) <-> ( D e. Poset /\ ( dom ( meet ` O ) = ( ( Base ` O ) X. ( Base ` O ) ) /\ dom ( join ` O ) = ( ( Base ` O ) X. ( Base ` O ) ) ) ) ) )`
6 eqid
` |-  ( Base ` O ) = ( Base ` O )`
7 eqid
` |-  ( join ` O ) = ( join ` O )`
8 eqid
` |-  ( meet ` O ) = ( meet ` O )`
9 6 7 8 islat
` |-  ( O e. Lat <-> ( O e. Poset /\ ( dom ( join ` O ) = ( ( Base ` O ) X. ( Base ` O ) ) /\ dom ( meet ` O ) = ( ( Base ` O ) X. ( Base ` O ) ) ) ) )`
10 1 6 odubas
` |-  ( Base ` O ) = ( Base ` D )`
11 1 8 odujoin
` |-  ( meet ` O ) = ( join ` D )`
12 1 7 odumeet
` |-  ( join ` O ) = ( meet ` D )`
13 10 11 12 islat
` |-  ( D e. Lat <-> ( D e. Poset /\ ( dom ( meet ` O ) = ( ( Base ` O ) X. ( Base ` O ) ) /\ dom ( join ` O ) = ( ( Base ` O ) X. ( Base ` O ) ) ) ) )`
14 5 9 13 3bitr4g
` |-  ( O e. V -> ( O e. Lat <-> D e. Lat ) )`