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	⊢ 𝐷 = ( ODual ‘ 𝑂 )
	odujoin.m	⊢ ∧ = ( meet ‘ 𝑂 )
Assertion	odujoin	⊢ ∧ = ( join ‘ 𝐷 )

Proof

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