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 ∈ CLat ↔ D ∈ CLat

Proof

Step Hyp Ref Expression
1 oduglb.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 syl5eq ⊢ ¬ 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 = 𝒫 Base O ∧ dom ⁡ glb ⁡ O = 𝒫 Base O ↔ dom ⁡ glb ⁡ O = 𝒫 Base O ∧ dom ⁡ lub ⁡ O = 𝒫 Base O
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 = 𝒫 Base O ↔ dom ⁡ lub ⁡ D = 𝒫 Base O
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 = 𝒫 Base O ↔ dom ⁡ glb ⁡ D = 𝒫 Base O
25 20 24 anbi12d ⊢ O ∈ V → dom ⁡ glb ⁡ O = 𝒫 Base O ∧ dom ⁡ lub ⁡ O = 𝒫 Base O ↔ dom ⁡ lub ⁡ D = 𝒫 Base O ∧ dom ⁡ glb ⁡ D = 𝒫 Base O
26 16 25 syl5bb ⊢ O ∈ V → dom ⁡ lub ⁡ O = 𝒫 Base O ∧ dom ⁡ glb ⁡ O = 𝒫 Base O ↔ dom ⁡ lub ⁡ D = 𝒫 Base O ∧ dom ⁡ glb ⁡ D = 𝒫 Base O
27 15 26 anbi12d ⊢ O ∈ V → O ∈ Poset ∧ dom ⁡ lub ⁡ O = 𝒫 Base O ∧ dom ⁡ glb ⁡ O = 𝒫 Base O ↔ D ∈ Poset ∧ dom ⁡ lub ⁡ D = 𝒫 Base O ∧ dom ⁡ glb ⁡ D = 𝒫 Base O
28 eqid ⊢ Base O = Base O
29 28 21 17 isclat ⊢ O ∈ CLat ↔ O ∈ Poset ∧ dom ⁡ lub ⁡ O = 𝒫 Base O ∧ dom ⁡ glb ⁡ O = 𝒫 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 ∈ CLat ↔ D ∈ Poset ∧ dom ⁡ lub ⁡ D = 𝒫 Base O ∧ dom ⁡ glb ⁡ D = 𝒫 Base O
34 27 29 33 3bitr4g ⊢ O ∈ V → O ∈ CLat ↔ D ∈ CLat
35 2 14 34 pm5.21nii ⊢ O ∈ CLat ↔ D ∈ CLat