Metamath Proof Explorer


Theorem odulatb

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

Ref Expression
Hypothesis odulat.d
|- D = ( ODual ` O )
Assertion odulatb
|- ( O e. V -> ( O e. Lat <-> D e. Lat ) )

Proof

Step Hyp Ref Expression
1 odulat.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 ) )