Metamath Proof Explorer

Theorem odulat

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

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

Proof

Step Hyp Ref Expression
1 oduglb.d 
 |-  D = ( ODual ` O )
2 1 odulatb 
 |-  ( O e. Lat -> ( O e. Lat <-> D e. Lat ) )
3 2 ibi 
 |-  ( O e. Lat -> D e. Lat )