# Metamath Proof Explorer

## Theorem oduclatb

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

Ref Expression
Hypothesis oduglb.d
`|- D = ( ODual ` O )`
Assertion oduclatb
`|- ( O e. CLat <-> D e. CLat )`

### Proof

Step Hyp Ref Expression
1 oduglb.d
` |-  D = ( ODual ` O )`
2 elex
` |-  ( O e. CLat -> O e. _V )`
3 noel
` |-  -. ( ( lub ` (/) ) ` (/) ) e. (/)`
4 ssid
` |-  (/) C_ (/)`
5 base0
` |-  (/) = ( Base ` (/) )`
6 eqid
` |-  ( lub ` (/) ) = ( lub ` (/) )`
7 5 6 clatlubcl
` |-  ( ( (/) e. CLat /\ (/) C_ (/) ) -> ( ( lub ` (/) ) ` (/) ) e. (/) )`
8 4 7 mpan2
` |-  ( (/) e. CLat -> ( ( lub ` (/) ) ` (/) ) e. (/) )`
9 3 8 mto
` |-  -. (/) e. CLat`
10 fvprc
` |-  ( -. O e. _V -> ( ODual ` O ) = (/) )`
11 1 10 syl5eq
` |-  ( -. O e. _V -> D = (/) )`
12 11 eleq1d
` |-  ( -. O e. _V -> ( D e. CLat <-> (/) e. CLat ) )`
13 9 12 mtbiri
` |-  ( -. O e. _V -> -. D e. CLat )`
14 13 con4i
` |-  ( D e. CLat -> O e. _V )`
15 1 oduposb
` |-  ( O e. _V -> ( O e. Poset <-> D e. Poset ) )`
16 ancom
` |-  ( ( dom ( lub ` O ) = ~P ( Base ` O ) /\ dom ( glb ` O ) = ~P ( Base ` O ) ) <-> ( dom ( glb ` O ) = ~P ( Base ` O ) /\ dom ( lub ` O ) = ~P ( Base ` O ) ) )`
17 eqid
` |-  ( glb ` O ) = ( glb ` O )`
18 1 17 odulub
` |-  ( O e. _V -> ( glb ` O ) = ( lub ` D ) )`
19 18 dmeqd
` |-  ( O e. _V -> dom ( glb ` O ) = dom ( lub ` D ) )`
20 19 eqeq1d
` |-  ( O e. _V -> ( dom ( glb ` O ) = ~P ( Base ` O ) <-> dom ( lub ` D ) = ~P ( Base ` O ) ) )`
21 eqid
` |-  ( lub ` O ) = ( lub ` O )`
22 1 21 oduglb
` |-  ( O e. _V -> ( lub ` O ) = ( glb ` D ) )`
23 22 dmeqd
` |-  ( O e. _V -> dom ( lub ` O ) = dom ( glb ` D ) )`
24 23 eqeq1d
` |-  ( O e. _V -> ( dom ( lub ` O ) = ~P ( Base ` O ) <-> dom ( glb ` D ) = ~P ( Base ` O ) ) )`
25 20 24 anbi12d
` |-  ( O e. _V -> ( ( dom ( glb ` O ) = ~P ( Base ` O ) /\ dom ( lub ` O ) = ~P ( Base ` O ) ) <-> ( dom ( lub ` D ) = ~P ( Base ` O ) /\ dom ( glb ` D ) = ~P ( Base ` O ) ) ) )`
26 16 25 syl5bb
` |-  ( O e. _V -> ( ( dom ( lub ` O ) = ~P ( Base ` O ) /\ dom ( glb ` O ) = ~P ( Base ` O ) ) <-> ( dom ( lub ` D ) = ~P ( Base ` O ) /\ dom ( glb ` D ) = ~P ( Base ` O ) ) ) )`
27 15 26 anbi12d
` |-  ( O e. _V -> ( ( O e. Poset /\ ( dom ( lub ` O ) = ~P ( Base ` O ) /\ dom ( glb ` O ) = ~P ( Base ` O ) ) ) <-> ( D e. Poset /\ ( dom ( lub ` D ) = ~P ( Base ` O ) /\ dom ( glb ` D ) = ~P ( Base ` O ) ) ) ) )`
28 eqid
` |-  ( Base ` O ) = ( Base ` O )`
29 28 21 17 isclat
` |-  ( O e. CLat <-> ( O e. Poset /\ ( dom ( lub ` O ) = ~P ( Base ` O ) /\ dom ( glb ` O ) = ~P ( Base ` O ) ) ) )`
30 1 28 odubas
` |-  ( Base ` O ) = ( Base ` D )`
31 eqid
` |-  ( lub ` D ) = ( lub ` D )`
32 eqid
` |-  ( glb ` D ) = ( glb ` D )`
33 30 31 32 isclat
` |-  ( D e. CLat <-> ( D e. Poset /\ ( dom ( lub ` D ) = ~P ( Base ` O ) /\ dom ( glb ` D ) = ~P ( Base ` O ) ) ) )`
34 27 29 33 3bitr4g
` |-  ( O e. _V -> ( O e. CLat <-> D e. CLat ) )`
35 2 14 34 pm5.21nii
` |-  ( O e. CLat <-> D e. CLat )`