# Metamath Proof Explorer

## 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
Assertion odujoin

### Proof

Step Hyp Ref Expression
1 oduglb.d ${⊢}{D}=\mathrm{ODual}\left({O}\right)$
2 odujoin.m
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}↔\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 ${⊢}¬{O}\in \mathrm{V}\to \mathrm{meet}\left({O}\right)=\varnothing$
16 fvprc ${⊢}¬{O}\in \mathrm{V}\to \mathrm{ODual}\left({O}\right)=\varnothing$
17 1 16 syl5eq ${⊢}¬{O}\in \mathrm{V}\to {D}=\varnothing$
18 17 fveq2d ${⊢}¬{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 syl6eq ${⊢}¬{O}\in \mathrm{V}\to \mathrm{join}\left({D}\right)=\varnothing$
21 15 20 eqtr4d ${⊢}¬{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