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

Proof

Step Hyp Ref Expression
1 oduclatb.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 eqtrid ⊢ ( ¬ 𝑂 ∈ 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 )