Metamath Proof Explorer

Theorem odumeet

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

Ref Expression
Hypotheses oduglb.d 𝐷 = ( ODual ‘ 𝑂 )
odumeet.j = ( join ‘ 𝑂 )
Assertion odumeet = ( meet ‘ 𝐷 )

Proof

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