Metamath Proof Explorer


Theorem odulatb

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

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

Proof

Step Hyp Ref Expression
1 odulat.d 𝐷 = ( ODual ‘ 𝑂 )
2 1 oduposb ( 𝑂𝑉 → ( 𝑂 ∈ Poset ↔ 𝐷 ∈ Poset ) )
3 ancom ( ( dom ( join ‘ 𝑂 ) = ( ( Base ‘ 𝑂 ) × ( Base ‘ 𝑂 ) ) ∧ dom ( meet ‘ 𝑂 ) = ( ( Base ‘ 𝑂 ) × ( Base ‘ 𝑂 ) ) ) ↔ ( dom ( meet ‘ 𝑂 ) = ( ( Base ‘ 𝑂 ) × ( Base ‘ 𝑂 ) ) ∧ dom ( join ‘ 𝑂 ) = ( ( Base ‘ 𝑂 ) × ( Base ‘ 𝑂 ) ) ) )
4 3 a1i ( 𝑂𝑉 → ( ( dom ( join ‘ 𝑂 ) = ( ( Base ‘ 𝑂 ) × ( Base ‘ 𝑂 ) ) ∧ dom ( meet ‘ 𝑂 ) = ( ( Base ‘ 𝑂 ) × ( Base ‘ 𝑂 ) ) ) ↔ ( dom ( meet ‘ 𝑂 ) = ( ( Base ‘ 𝑂 ) × ( Base ‘ 𝑂 ) ) ∧ dom ( join ‘ 𝑂 ) = ( ( Base ‘ 𝑂 ) × ( Base ‘ 𝑂 ) ) ) ) )
5 2 4 anbi12d ( 𝑂𝑉 → ( ( 𝑂 ∈ Poset ∧ ( dom ( join ‘ 𝑂 ) = ( ( Base ‘ 𝑂 ) × ( Base ‘ 𝑂 ) ) ∧ dom ( meet ‘ 𝑂 ) = ( ( Base ‘ 𝑂 ) × ( Base ‘ 𝑂 ) ) ) ) ↔ ( 𝐷 ∈ Poset ∧ ( dom ( meet ‘ 𝑂 ) = ( ( Base ‘ 𝑂 ) × ( Base ‘ 𝑂 ) ) ∧ dom ( join ‘ 𝑂 ) = ( ( Base ‘ 𝑂 ) × ( Base ‘ 𝑂 ) ) ) ) ) )
6 eqid ( Base ‘ 𝑂 ) = ( Base ‘ 𝑂 )
7 eqid ( join ‘ 𝑂 ) = ( join ‘ 𝑂 )
8 eqid ( meet ‘ 𝑂 ) = ( meet ‘ 𝑂 )
9 6 7 8 islat ( 𝑂 ∈ Lat ↔ ( 𝑂 ∈ Poset ∧ ( dom ( join ‘ 𝑂 ) = ( ( Base ‘ 𝑂 ) × ( Base ‘ 𝑂 ) ) ∧ dom ( meet ‘ 𝑂 ) = ( ( Base ‘ 𝑂 ) × ( Base ‘ 𝑂 ) ) ) ) )
10 1 6 odubas ( Base ‘ 𝑂 ) = ( Base ‘ 𝐷 )
11 1 8 odujoin ( meet ‘ 𝑂 ) = ( join ‘ 𝐷 )
12 1 7 odumeet ( join ‘ 𝑂 ) = ( meet ‘ 𝐷 )
13 10 11 12 islat ( 𝐷 ∈ Lat ↔ ( 𝐷 ∈ Poset ∧ ( dom ( meet ‘ 𝑂 ) = ( ( Base ‘ 𝑂 ) × ( Base ‘ 𝑂 ) ) ∧ dom ( join ‘ 𝑂 ) = ( ( Base ‘ 𝑂 ) × ( Base ‘ 𝑂 ) ) ) ) )
14 5 9 13 3bitr4g ( 𝑂𝑉 → ( 𝑂 ∈ Lat ↔ 𝐷 ∈ Lat ) )