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 ‘ 𝐷 )