# 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 𝐷 = ( ODual ‘ 𝑂 )
odujoin.m = ( meet ‘ 𝑂 )
Assertion odujoin = ( join ‘ 𝐷 )

### Proof

Step Hyp Ref Expression
1 oduglb.d 𝐷 = ( ODual ‘ 𝑂 )
2 odujoin.m = ( meet ‘ 𝑂 )
3 eqid ( glb ‘ 𝑂 ) = ( glb ‘ 𝑂 )
4 1 3 odulub ( 𝑂 ∈ V → ( glb ‘ 𝑂 ) = ( lub ‘ 𝐷 ) )
5 4 breqd ( 𝑂 ∈ V → ( { 𝑎 , 𝑏 } ( glb ‘ 𝑂 ) 𝑐 ↔ { 𝑎 , 𝑏 } ( lub ‘ 𝐷 ) 𝑐 ) )
6 5 oprabbidv ( 𝑂 ∈ V → { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ∣ { 𝑎 , 𝑏 } ( glb ‘ 𝑂 ) 𝑐 } = { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ∣ { 𝑎 , 𝑏 } ( lub ‘ 𝐷 ) 𝑐 } )
7 eqid ( meet ‘ 𝑂 ) = ( meet ‘ 𝑂 )
8 3 7 meetfval ( 𝑂 ∈ V → ( meet ‘ 𝑂 ) = { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ∣ { 𝑎 , 𝑏 } ( glb ‘ 𝑂 ) 𝑐 } )
9 1 fvexi 𝐷 ∈ V
10 eqid ( lub ‘ 𝐷 ) = ( lub ‘ 𝐷 )
11 eqid ( join ‘ 𝐷 ) = ( join ‘ 𝐷 )
12 10 11 joinfval ( 𝐷 ∈ V → ( join ‘ 𝐷 ) = { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ∣ { 𝑎 , 𝑏 } ( lub ‘ 𝐷 ) 𝑐 } )
13 9 12 mp1i ( 𝑂 ∈ V → ( join ‘ 𝐷 ) = { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ∣ { 𝑎 , 𝑏 } ( lub ‘ 𝐷 ) 𝑐 } )
14 6 8 13 3eqtr4d ( 𝑂 ∈ V → ( meet ‘ 𝑂 ) = ( join ‘ 𝐷 ) )
15 fvprc ( ¬ 𝑂 ∈ V → ( meet ‘ 𝑂 ) = ∅ )
16 fvprc ( ¬ 𝑂 ∈ V → ( ODual ‘ 𝑂 ) = ∅ )
17 1 16 syl5eq ( ¬ 𝑂 ∈ V → 𝐷 = ∅ )
18 17 fveq2d ( ¬ 𝑂 ∈ V → ( join ‘ 𝐷 ) = ( join ‘ ∅ ) )
19 join0 ( join ‘ ∅ ) = ∅
20 18 19 eqtrdi ( ¬ 𝑂 ∈ V → ( join ‘ 𝐷 ) = ∅ )
21 15 20 eqtr4d ( ¬ 𝑂 ∈ V → ( meet ‘ 𝑂 ) = ( join ‘ 𝐷 ) )
22 14 21 pm2.61i ( meet ‘ 𝑂 ) = ( join ‘ 𝐷 )
23 2 22 eqtri = ( join ‘ 𝐷 )