This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
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 ‘ 𝐷 ) |
| 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 | eqtrid | ⊢ ( ¬ 𝑂 ∈ 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 ‘ 𝐷 ) |