odulatb

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

		Ref	Expression
	Hypothesis	odulat.d	$⊢ D = ODual (O)$
	Assertion	odulatb	$⊢ O \in V \to (O \in Lat \leftrightarrow D \in Lat)$

Step	Hyp	Ref	Expression
1		odulat.d	$⊢ D = ODual (O)$
2	1	oduposb	$⊢ O \in V \to (O \in Poset \leftrightarrow D \in Poset)$
3		ancom	$⊢ (dom join (O) = {Base}_{O} \times {Base}_{O} \land dom meet (O) = {Base}_{O} \times {Base}_{O}) \leftrightarrow (dom meet (O) = {Base}_{O} \times {Base}_{O} \land dom join (O) = {Base}_{O} \times {Base}_{O})$
4	3	a1i	$⊢ O \in V \to ((dom join (O) = {Base}_{O} \times {Base}_{O} \land dom meet (O) = {Base}_{O} \times {Base}_{O}) \leftrightarrow (dom meet (O) = {Base}_{O} \times {Base}_{O} \land dom join (O) = {Base}_{O} \times {Base}_{O}))$
5	2 4	anbi12d	$⊢ O \in V \to ((O \in Poset \land (dom join (O) = {Base}_{O} \times {Base}_{O} \land dom meet (O) = {Base}_{O} \times {Base}_{O})) \leftrightarrow (D \in Poset \land (dom meet (O) = {Base}_{O} \times {Base}_{O} \land dom join (O) = {Base}_{O} \times {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 \in Lat \leftrightarrow (O \in Poset \land (dom join (O) = {Base}_{O} \times {Base}_{O} \land dom meet (O) = {Base}_{O} \times {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 \in Lat \leftrightarrow (D \in Poset \land (dom meet (O) = {Base}_{O} \times {Base}_{O} \land dom join (O) = {Base}_{O} \times {Base}_{O}))$
14	5 9 13	3bitr4g	$⊢ O \in V \to (O \in Lat \leftrightarrow D \in Lat)$

Metamath Proof Explorer