Metamath Proof Explorer

Theorem oduclatb

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

Ref Expression
Hypothesis oduclatb.d ⊢D=ODual⁡O
Assertion oduclatb ⊢O∈CLat↔D∈CLat

Proof

Step Hyp Ref Expression
1 oduclatb.d ⊢D=ODual⁡O
2 elex ⊢O∈CLat→O∈V
3 noel ⊢¬lub⁡∅⁡∅∈∅
4 ssid ⊢∅⊆∅
5 base0 ⊢∅=Base∅
6 eqid ⊢lub⁡∅=lub⁡∅
7 5 6 clatlubcl ⊢∅∈CLat∧∅⊆∅→lub⁡∅⁡∅∈∅
8 4 7 mpan2 ⊢∅∈CLat→lub⁡∅⁡∅∈∅
9 3 8 mto ⊢¬∅∈CLat
10 fvprc ⊢¬O∈V→ODual⁡O=∅
11 1 10 eqtrid ⊢¬O∈V→D=∅
12 11 eleq1d ⊢¬O∈V→D∈CLat↔∅∈CLat
13 9 12 mtbiri ⊢¬O∈V→¬D∈CLat
14 13 con4i ⊢D∈CLat→O∈V
15 1 oduposb ⊢O∈V→O∈Poset↔D∈Poset
16 ancom ⊢dom⁡lub⁡O=𝒫BaseO∧dom⁡glb⁡O=𝒫BaseO↔dom⁡glb⁡O=𝒫BaseO∧dom⁡lub⁡O=𝒫BaseO
17 eqid ⊢glb⁡O=glb⁡O
18 1 17 odulub ⊢O∈V→glb⁡O=lub⁡D
19 18 dmeqd ⊢O∈V→dom⁡glb⁡O=dom⁡lub⁡D
20 19 eqeq1d ⊢O∈V→dom⁡glb⁡O=𝒫BaseO↔dom⁡lub⁡D=𝒫BaseO
21 eqid ⊢lub⁡O=lub⁡O
22 1 21 oduglb ⊢O∈V→lub⁡O=glb⁡D
23 22 dmeqd ⊢O∈V→dom⁡lub⁡O=dom⁡glb⁡D
24 23 eqeq1d ⊢O∈V→dom⁡lub⁡O=𝒫BaseO↔dom⁡glb⁡D=𝒫BaseO
25 20 24 anbi12d ⊢O∈V→dom⁡glb⁡O=𝒫BaseO∧dom⁡lub⁡O=𝒫BaseO↔dom⁡lub⁡D=𝒫BaseO∧dom⁡glb⁡D=𝒫BaseO
26 16 25 bitrid ⊢O∈V→dom⁡lub⁡O=𝒫BaseO∧dom⁡glb⁡O=𝒫BaseO↔dom⁡lub⁡D=𝒫BaseO∧dom⁡glb⁡D=𝒫BaseO
27 15 26 anbi12d ⊢O∈V→O∈Poset∧dom⁡lub⁡O=𝒫BaseO∧dom⁡glb⁡O=𝒫BaseO↔D∈Poset∧dom⁡lub⁡D=𝒫BaseO∧dom⁡glb⁡D=𝒫BaseO
28 eqid ⊢BaseO=BaseO
29 28 21 17 isclat ⊢O∈CLat↔O∈Poset∧dom⁡lub⁡O=𝒫BaseO∧dom⁡glb⁡O=𝒫BaseO
30 1 28 odubas ⊢BaseO=BaseD
31 eqid ⊢lub⁡D=lub⁡D
32 eqid ⊢glb⁡D=glb⁡D
33 30 31 32 isclat ⊢D∈CLat↔D∈Poset∧dom⁡lub⁡D=𝒫BaseO∧dom⁡glb⁡D=𝒫BaseO
34 27 29 33 3bitr4g ⊢O∈V→O∈CLat↔D∈CLat
35 2 14 34 pm5.21nii ⊢O∈CLat↔D∈CLat