# 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 𝐷 = ( ODual ‘ 𝑂 )
Assertion oduclatb ( 𝑂 ∈ CLat ↔ 𝐷 ∈ CLat )

### Proof

Step Hyp Ref Expression
1 oduglb.d 𝐷 = ( ODual ‘ 𝑂 )
2 elex ( 𝑂 ∈ CLat → 𝑂 ∈ 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 ( ¬ 𝑂 ∈ V → ( ODual ‘ 𝑂 ) = ∅ )
11 1 10 syl5eq ( ¬ 𝑂 ∈ V → 𝐷 = ∅ )
12 11 eleq1d ( ¬ 𝑂 ∈ V → ( 𝐷 ∈ CLat ↔ ∅ ∈ CLat ) )
13 9 12 mtbiri ( ¬ 𝑂 ∈ V → ¬ 𝐷 ∈ CLat )
14 13 con4i ( 𝐷 ∈ CLat → 𝑂 ∈ V )
15 1 oduposb ( 𝑂 ∈ V → ( 𝑂 ∈ Poset ↔ 𝐷 ∈ Poset ) )
16 ancom ( ( dom ( lub ‘ 𝑂 ) = 𝒫 ( Base ‘ 𝑂 ) ∧ dom ( glb ‘ 𝑂 ) = 𝒫 ( Base ‘ 𝑂 ) ) ↔ ( dom ( glb ‘ 𝑂 ) = 𝒫 ( Base ‘ 𝑂 ) ∧ dom ( lub ‘ 𝑂 ) = 𝒫 ( Base ‘ 𝑂 ) ) )
17 eqid ( glb ‘ 𝑂 ) = ( glb ‘ 𝑂 )
18 1 17 odulub ( 𝑂 ∈ V → ( glb ‘ 𝑂 ) = ( lub ‘ 𝐷 ) )
19 18 dmeqd ( 𝑂 ∈ V → dom ( glb ‘ 𝑂 ) = dom ( lub ‘ 𝐷 ) )
20 19 eqeq1d ( 𝑂 ∈ V → ( dom ( glb ‘ 𝑂 ) = 𝒫 ( Base ‘ 𝑂 ) ↔ dom ( lub ‘ 𝐷 ) = 𝒫 ( Base ‘ 𝑂 ) ) )
21 eqid ( lub ‘ 𝑂 ) = ( lub ‘ 𝑂 )
22 1 21 oduglb ( 𝑂 ∈ V → ( lub ‘ 𝑂 ) = ( glb ‘ 𝐷 ) )
23 22 dmeqd ( 𝑂 ∈ V → dom ( lub ‘ 𝑂 ) = dom ( glb ‘ 𝐷 ) )
24 23 eqeq1d ( 𝑂 ∈ V → ( dom ( lub ‘ 𝑂 ) = 𝒫 ( Base ‘ 𝑂 ) ↔ dom ( glb ‘ 𝐷 ) = 𝒫 ( Base ‘ 𝑂 ) ) )
25 20 24 anbi12d ( 𝑂 ∈ V → ( ( dom ( glb ‘ 𝑂 ) = 𝒫 ( Base ‘ 𝑂 ) ∧ dom ( lub ‘ 𝑂 ) = 𝒫 ( Base ‘ 𝑂 ) ) ↔ ( dom ( lub ‘ 𝐷 ) = 𝒫 ( Base ‘ 𝑂 ) ∧ dom ( glb ‘ 𝐷 ) = 𝒫 ( Base ‘ 𝑂 ) ) ) )
26 16 25 syl5bb ( 𝑂 ∈ V → ( ( dom ( lub ‘ 𝑂 ) = 𝒫 ( Base ‘ 𝑂 ) ∧ dom ( glb ‘ 𝑂 ) = 𝒫 ( Base ‘ 𝑂 ) ) ↔ ( dom ( lub ‘ 𝐷 ) = 𝒫 ( Base ‘ 𝑂 ) ∧ dom ( glb ‘ 𝐷 ) = 𝒫 ( Base ‘ 𝑂 ) ) ) )
27 15 26 anbi12d ( 𝑂 ∈ V → ( ( 𝑂 ∈ Poset ∧ ( dom ( lub ‘ 𝑂 ) = 𝒫 ( Base ‘ 𝑂 ) ∧ dom ( glb ‘ 𝑂 ) = 𝒫 ( Base ‘ 𝑂 ) ) ) ↔ ( 𝐷 ∈ Poset ∧ ( dom ( lub ‘ 𝐷 ) = 𝒫 ( Base ‘ 𝑂 ) ∧ dom ( glb ‘ 𝐷 ) = 𝒫 ( Base ‘ 𝑂 ) ) ) ) )
28 eqid ( Base ‘ 𝑂 ) = ( Base ‘ 𝑂 )
29 28 21 17 isclat ( 𝑂 ∈ CLat ↔ ( 𝑂 ∈ Poset ∧ ( dom ( lub ‘ 𝑂 ) = 𝒫 ( Base ‘ 𝑂 ) ∧ dom ( glb ‘ 𝑂 ) = 𝒫 ( Base ‘ 𝑂 ) ) ) )
30 1 28 odubas ( Base ‘ 𝑂 ) = ( Base ‘ 𝐷 )
31 eqid ( lub ‘ 𝐷 ) = ( lub ‘ 𝐷 )
32 eqid ( glb ‘ 𝐷 ) = ( glb ‘ 𝐷 )
33 30 31 32 isclat ( 𝐷 ∈ CLat ↔ ( 𝐷 ∈ Poset ∧ ( dom ( lub ‘ 𝐷 ) = 𝒫 ( Base ‘ 𝑂 ) ∧ dom ( glb ‘ 𝐷 ) = 𝒫 ( Base ‘ 𝑂 ) ) ) )
34 27 29 33 3bitr4g ( 𝑂 ∈ V → ( 𝑂 ∈ CLat ↔ 𝐷 ∈ CLat ) )
35 2 14 34 pm5.21nii ( 𝑂 ∈ CLat ↔ 𝐷 ∈ CLat )