This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqtrid ⊢ ( ¬ 𝑂 ∈ 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 ‘ 𝐷 )