Metamath Proof Explorer


Theorem odulat

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

Ref Expression
Hypothesis odulat.d 𝐷 = ( ODual ‘ 𝑂 )
Assertion odulat ( 𝑂 ∈ Lat → 𝐷 ∈ Lat )

Proof

Step Hyp Ref Expression
1 odulat.d 𝐷 = ( ODual ‘ 𝑂 )
2 1 odulatb ( 𝑂 ∈ Lat → ( 𝑂 ∈ Lat ↔ 𝐷 ∈ Lat ) )
3 2 ibi ( 𝑂 ∈ Lat → 𝐷 ∈ Lat )