This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )