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