Metamath Proof Explorer

Theorem odulatb

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

Ref Expression
Hypothesis oduglb.d ⊢ D = ODual ⁡ O
Assertion odulatb ⊢ O ∈ V → O ∈ Lat ↔ D ∈ Lat

Proof

Step Hyp Ref Expression
1 oduglb.d ⊢ D = ODual ⁡ O
2 1 oduposb ⊢ O ∈ V → O ∈ Poset ↔ D ∈ Poset
3 ancom ⊢ dom ⁡ join ⁡ O = Base O × Base O ∧ dom ⁡ meet ⁡ O = Base O × Base O ↔ dom ⁡ meet ⁡ O = Base O × Base O ∧ dom ⁡ join ⁡ O = Base O × Base O
4 3 a1i ⊢ O ∈ V → dom ⁡ join ⁡ O = Base O × Base O ∧ dom ⁡ meet ⁡ O = Base O × Base O ↔ dom ⁡ meet ⁡ O = Base O × Base O ∧ dom ⁡ join ⁡ O = Base O × Base O
5 2 4 anbi12d ⊢ O ∈ V → O ∈ Poset ∧ dom ⁡ join ⁡ O = Base O × Base O ∧ dom ⁡ meet ⁡ O = Base O × Base O ↔ D ∈ Poset ∧ dom ⁡ meet ⁡ O = Base O × Base O ∧ dom ⁡ join ⁡ O = Base O × Base O
6 eqid ⊢ Base O = Base O
7 eqid ⊢ join ⁡ O = join ⁡ O
8 eqid ⊢ meet ⁡ O = meet ⁡ O
9 6 7 8 islat ⊢ O ∈ Lat ↔ O ∈ Poset ∧ dom ⁡ join ⁡ O = Base O × Base O ∧ dom ⁡ meet ⁡ O = Base O × Base O
10 1 6 odubas ⊢ Base O = Base D
11 1 8 odujoin ⊢ meet ⁡ O = join ⁡ D
12 1 7 odumeet ⊢ join ⁡ O = meet ⁡ D
13 10 11 12 islat ⊢ D ∈ Lat ↔ D ∈ Poset ∧ dom ⁡ meet ⁡ O = Base O × Base O ∧ dom ⁡ join ⁡ O = Base O × Base O
14 5 9 13 3bitr4g ⊢ O ∈ V → O ∈ Lat ↔ D ∈ Lat