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 = ODual ⁡ O
odujoin.m ⊢ ∧ ˙ = meet ⁡ O
Assertion odujoin ⊢ ∧ ˙ = join ⁡ D

Proof

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