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 ) )