Theorem odujoin

Description: Joins in a dual order are meets in the original. (Contributed by Stefan O'Rear, 29-Jan-2015)

	Ref	Expression
Hypotheses	oduglb.d	$$⊢D=\mathrm{ODual}\left(O\right)$$
	odujoin.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(O\right)$$
Assertion	odujoin	$$⊢\underset{\dot{}}{\wedge }=\mathrm{join}\left(D\right)$$

Proof

Step	Hyp	Ref	Expression
1		oduglb.d	$$⊢D=\mathrm{ODual}\left(O\right)$$
2		odujoin.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(O\right)$$
3		eqid	$$⊢\mathrm{glb}\left(O\right)=\mathrm{glb}\left(O\right)$$
4	1 3	odulub	$$⊢O\in \mathrm{V}\to \mathrm{glb}\left(O\right)=\mathrm{lub}\left(D\right)$$
5	4	breqd	$$⊢O\in \mathrm{V}\to \left(\left\{a,b\right\}\mathrm{glb}\left(O\right)c\leftrightarrow \left\{a,b\right\}\mathrm{lub}\left(D\right)c\right)$$
6	5	oprabbidv	$$⊢O\in \mathrm{V}\to \left\{⟨⟨a,b⟩,c⟩|\left\{a,b\right\}\mathrm{glb}\left(O\right)c\right\}=\left\{⟨⟨a,b⟩,c⟩|\left\{a,b\right\}\mathrm{lub}\left(D\right)c\right\}$$
7		eqid	$$⊢\mathrm{meet}\left(O\right)=\mathrm{meet}\left(O\right)$$
8	3 7	meetfval	$$⊢O\in \mathrm{V}\to \mathrm{meet}\left(O\right)=\left\{⟨⟨a,b⟩,c⟩|\left\{a,b\right\}\mathrm{glb}\left(O\right)c\right\}$$
9	1	fvexi	$$⊢D\in \mathrm{V}$$
10		eqid	$$⊢\mathrm{lub}\left(D\right)=\mathrm{lub}\left(D\right)$$
11		eqid	$$⊢\mathrm{join}\left(D\right)=\mathrm{join}\left(D\right)$$
12	10 11	joinfval	$$⊢D\in \mathrm{V}\to \mathrm{join}\left(D\right)=\left\{⟨⟨a,b⟩,c⟩|\left\{a,b\right\}\mathrm{lub}\left(D\right)c\right\}$$
13	9 12	mp1i	$$⊢O\in \mathrm{V}\to \mathrm{join}\left(D\right)=\left\{⟨⟨a,b⟩,c⟩|\left\{a,b\right\}\mathrm{lub}\left(D\right)c\right\}$$
14	6 8 13	3eqtr4d	$$⊢O\in \mathrm{V}\to \mathrm{meet}\left(O\right)=\mathrm{join}\left(D\right)$$
15		fvprc	$$⊢\neg O\in \mathrm{V}\to \mathrm{meet}\left(O\right)=\varnothing$$
16		fvprc	$$⊢\neg O\in \mathrm{V}\to \mathrm{ODual}\left(O\right)=\varnothing$$
17	1 16	eqtrid	$$⊢\neg O\in \mathrm{V}\to D=\varnothing$$
18	17	fveq2d	$$⊢\neg O\in \mathrm{V}\to \mathrm{join}\left(D\right)=\mathrm{join}\left(\varnothing \right)$$
19		join0	$$⊢\mathrm{join}\left(\varnothing \right)=\varnothing$$
20	18 19	eqtrdi	$$⊢\neg O\in \mathrm{V}\to \mathrm{join}\left(D\right)=\varnothing$$
21	15 20	eqtr4d	$$⊢\neg O\in \mathrm{V}\to \mathrm{meet}\left(O\right)=\mathrm{join}\left(D\right)$$
22	14 21	pm2.61i	$$⊢\mathrm{meet}\left(O\right)=\mathrm{join}\left(D\right)$$
23	2 22	eqtri	$$⊢\underset{\dot{}}{\wedge }=\mathrm{join}\left(D\right)$$