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 ⊢ D = ODual ⁡ O
odumeet.j ⊢ ∨ ˙ = join ⁡ O
Assertion odumeet ⊢ ∨ ˙ = meet ⁡ D

Proof

Step Hyp Ref Expression
1 oduglb.d ⊢ D = ODual ⁡ O
2 odumeet.j ⊢ ∨ ˙ = join ⁡ O
3 eqid ⊢ lub ⁡ O = lub ⁡ O
4 1 3 oduglb ⊢ O ∈ V → lub ⁡ O = glb ⁡ D
5 4 breqd ⊢ O ∈ V → a b lub ⁡ O c ↔ a b glb ⁡ D c
6 5 oprabbidv ⊢ O ∈ V → a b c | a b lub ⁡ O c = a b c | a b glb ⁡ D c
7 eqid ⊢ join ⁡ O = join ⁡ O
8 3 7 joinfval ⊢ O ∈ V → join ⁡ O = a b c | a b lub ⁡ O c
9 1 fvexi ⊢ D ∈ V
10 eqid ⊢ glb ⁡ D = glb ⁡ D
11 eqid ⊢ meet ⁡ D = meet ⁡ D
12 10 11 meetfval ⊢ D ∈ V → meet ⁡ D = a b c | a b glb ⁡ D c
13 9 12 mp1i ⊢ O ∈ V → meet ⁡ D = a b c | a b glb ⁡ D c
14 6 8 13 3eqtr4d ⊢ O ∈ V → join ⁡ O = meet ⁡ D
15 fvprc ⊢ ¬ O ∈ V → join ⁡ O = ∅
16 fvprc ⊢ ¬ O ∈ V → ODual ⁡ O = ∅
17 1 16 syl5eq ⊢ ¬ O ∈ V → D = ∅
18 17 fveq2d ⊢ ¬ O ∈ V → meet ⁡ D = meet ⁡ ∅
19 meet0 ⊢ meet ⁡ ∅ = ∅
20 18 19 eqtrdi ⊢ ¬ O ∈ V → meet ⁡ D = ∅
21 15 20 eqtr4d ⊢ ¬ O ∈ V → join ⁡ O = meet ⁡ D
22 14 21 pm2.61i ⊢ join ⁡ O = meet ⁡ D
23 2 22 eqtri ⊢ ∨ ˙ = meet ⁡ D