Theorem odulub

Description: Least upper bounds in a dual order are greatest lower bounds in the original order. (Contributed by Stefan O'Rear, 29-Jan-2015)

	Ref	Expression
Hypotheses	oduglb.d	⊢ 𝐷 = ( ODual ‘ 𝑂 )
	odulub.l	⊢ 𝐿 = ( glb ‘ 𝑂 )
Assertion	odulub	⊢ ( 𝑂 ∈ 𝑉 → 𝐿 = ( lub ‘ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		oduglb.d	⊢ 𝐷 = ( ODual ‘ 𝑂 )
2		odulub.l	⊢ 𝐿 = ( glb ‘ 𝑂 )
3		vex	⊢ 𝑐 ∈ V
4		vex	⊢ 𝑏 ∈ V
5	3 4	brcnv	⊢ ( 𝑐 ◡ ( le ‘ 𝑂 ) 𝑏 ↔ 𝑏 ( le ‘ 𝑂 ) 𝑐 )
6	5	ralbii	⊢ ( ∀ 𝑐 ∈ 𝑎 𝑐 ◡ ( le ‘ 𝑂 ) 𝑏 ↔ ∀ 𝑐 ∈ 𝑎 𝑏 ( le ‘ 𝑂 ) 𝑐 )
7		vex	⊢ 𝑑 ∈ V
8	3 7	brcnv	⊢ ( 𝑐 ◡ ( le ‘ 𝑂 ) 𝑑 ↔ 𝑑 ( le ‘ 𝑂 ) 𝑐 )
9	8	ralbii	⊢ ( ∀ 𝑐 ∈ 𝑎 𝑐 ◡ ( le ‘ 𝑂 ) 𝑑 ↔ ∀ 𝑐 ∈ 𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐 )
10	4 7	brcnv	⊢ ( 𝑏 ◡ ( le ‘ 𝑂 ) 𝑑 ↔ 𝑑 ( le ‘ 𝑂 ) 𝑏 )
11	9 10	imbi12i	⊢ ( ( ∀ 𝑐 ∈ 𝑎 𝑐 ◡ ( le ‘ 𝑂 ) 𝑑 → 𝑏 ◡ ( le ‘ 𝑂 ) 𝑑 ) ↔ ( ∀ 𝑐 ∈ 𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐 → 𝑑 ( le ‘ 𝑂 ) 𝑏 ) )
12	11	ralbii	⊢ ( ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑐 ◡ ( le ‘ 𝑂 ) 𝑑 → 𝑏 ◡ ( le ‘ 𝑂 ) 𝑑 ) ↔ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐 → 𝑑 ( le ‘ 𝑂 ) 𝑏 ) )
13	6 12	anbi12i	⊢ ( ( ∀ 𝑐 ∈ 𝑎 𝑐 ◡ ( le ‘ 𝑂 ) 𝑏 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑐 ◡ ( le ‘ 𝑂 ) 𝑑 → 𝑏 ◡ ( le ‘ 𝑂 ) 𝑑 ) ) ↔ ( ∀ 𝑐 ∈ 𝑎 𝑏 ( le ‘ 𝑂 ) 𝑐 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐 → 𝑑 ( le ‘ 𝑂 ) 𝑏 ) ) )
14	13	a1i	⊢ ( 𝑏 ∈ ( Base ‘ 𝑂 ) → ( ( ∀ 𝑐 ∈ 𝑎 𝑐 ◡ ( le ‘ 𝑂 ) 𝑏 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑐 ◡ ( le ‘ 𝑂 ) 𝑑 → 𝑏 ◡ ( le ‘ 𝑂 ) 𝑑 ) ) ↔ ( ∀ 𝑐 ∈ 𝑎 𝑏 ( le ‘ 𝑂 ) 𝑐 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐 → 𝑑 ( le ‘ 𝑂 ) 𝑏 ) ) ) )
15	14	riotabiia	⊢ ( ℩ 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑐 ◡ ( le ‘ 𝑂 ) 𝑏 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑐 ◡ ( le ‘ 𝑂 ) 𝑑 → 𝑏 ◡ ( le ‘ 𝑂 ) 𝑑 ) ) ) = ( ℩ 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑏 ( le ‘ 𝑂 ) 𝑐 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐 → 𝑑 ( le ‘ 𝑂 ) 𝑏 ) ) )
16	15	mpteq2i	⊢ ( 𝑎 ∈ 𝒫 ( Base ‘ 𝑂 ) ↦ ( ℩ 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑐 ◡ ( le ‘ 𝑂 ) 𝑏 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑐 ◡ ( le ‘ 𝑂 ) 𝑑 → 𝑏 ◡ ( le ‘ 𝑂 ) 𝑑 ) ) ) ) = ( 𝑎 ∈ 𝒫 ( Base ‘ 𝑂 ) ↦ ( ℩ 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑏 ( le ‘ 𝑂 ) 𝑐 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐 → 𝑑 ( le ‘ 𝑂 ) 𝑏 ) ) ) )
17	13	reubii	⊢ ( ∃! 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑐 ◡ ( le ‘ 𝑂 ) 𝑏 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑐 ◡ ( le ‘ 𝑂 ) 𝑑 → 𝑏 ◡ ( le ‘ 𝑂 ) 𝑑 ) ) ↔ ∃! 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑏 ( le ‘ 𝑂 ) 𝑐 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐 → 𝑑 ( le ‘ 𝑂 ) 𝑏 ) ) )
18	17	abbii	⊢ { 𝑎 ∣ ∃! 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑐 ◡ ( le ‘ 𝑂 ) 𝑏 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑐 ◡ ( le ‘ 𝑂 ) 𝑑 → 𝑏 ◡ ( le ‘ 𝑂 ) 𝑑 ) ) } = { 𝑎 ∣ ∃! 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑏 ( le ‘ 𝑂 ) 𝑐 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐 → 𝑑 ( le ‘ 𝑂 ) 𝑏 ) ) }
19	16 18	reseq12i	⊢ ( ( 𝑎 ∈ 𝒫 ( Base ‘ 𝑂 ) ↦ ( ℩ 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑐 ◡ ( le ‘ 𝑂 ) 𝑏 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑐 ◡ ( le ‘ 𝑂 ) 𝑑 → 𝑏 ◡ ( le ‘ 𝑂 ) 𝑑 ) ) ) ) ↾ { 𝑎 ∣ ∃! 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑐 ◡ ( le ‘ 𝑂 ) 𝑏 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑐 ◡ ( le ‘ 𝑂 ) 𝑑 → 𝑏 ◡ ( le ‘ 𝑂 ) 𝑑 ) ) } ) = ( ( 𝑎 ∈ 𝒫 ( Base ‘ 𝑂 ) ↦ ( ℩ 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑏 ( le ‘ 𝑂 ) 𝑐 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐 → 𝑑 ( le ‘ 𝑂 ) 𝑏 ) ) ) ) ↾ { 𝑎 ∣ ∃! 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑏 ( le ‘ 𝑂 ) 𝑐 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐 → 𝑑 ( le ‘ 𝑂 ) 𝑏 ) ) } )
20	19	eqcomi	⊢ ( ( 𝑎 ∈ 𝒫 ( Base ‘ 𝑂 ) ↦ ( ℩ 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑏 ( le ‘ 𝑂 ) 𝑐 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐 → 𝑑 ( le ‘ 𝑂 ) 𝑏 ) ) ) ) ↾ { 𝑎 ∣ ∃! 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑏 ( le ‘ 𝑂 ) 𝑐 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐 → 𝑑 ( le ‘ 𝑂 ) 𝑏 ) ) } ) = ( ( 𝑎 ∈ 𝒫 ( Base ‘ 𝑂 ) ↦ ( ℩ 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑐 ◡ ( le ‘ 𝑂 ) 𝑏 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑐 ◡ ( le ‘ 𝑂 ) 𝑑 → 𝑏 ◡ ( le ‘ 𝑂 ) 𝑑 ) ) ) ) ↾ { 𝑎 ∣ ∃! 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑐 ◡ ( le ‘ 𝑂 ) 𝑏 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑐 ◡ ( le ‘ 𝑂 ) 𝑑 → 𝑏 ◡ ( le ‘ 𝑂 ) 𝑑 ) ) } )
21		eqid	⊢ ( Base ‘ 𝑂 ) = ( Base ‘ 𝑂 )
22		eqid	⊢ ( le ‘ 𝑂 ) = ( le ‘ 𝑂 )
23		eqid	⊢ ( glb ‘ 𝑂 ) = ( glb ‘ 𝑂 )
24		biid	⊢ ( ( ∀ 𝑐 ∈ 𝑎 𝑏 ( le ‘ 𝑂 ) 𝑐 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐 → 𝑑 ( le ‘ 𝑂 ) 𝑏 ) ) ↔ ( ∀ 𝑐 ∈ 𝑎 𝑏 ( le ‘ 𝑂 ) 𝑐 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐 → 𝑑 ( le ‘ 𝑂 ) 𝑏 ) ) )
25		id	⊢ ( 𝑂 ∈ 𝑉 → 𝑂 ∈ 𝑉 )
26	21 22 23 24 25	glbfval	⊢ ( 𝑂 ∈ 𝑉 → ( glb ‘ 𝑂 ) = ( ( 𝑎 ∈ 𝒫 ( Base ‘ 𝑂 ) ↦ ( ℩ 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑏 ( le ‘ 𝑂 ) 𝑐 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐 → 𝑑 ( le ‘ 𝑂 ) 𝑏 ) ) ) ) ↾ { 𝑎 ∣ ∃! 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑏 ( le ‘ 𝑂 ) 𝑐 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑑 ( le ‘ 𝑂 ) 𝑐 → 𝑑 ( le ‘ 𝑂 ) 𝑏 ) ) } ) )
27	1	fvexi	⊢ 𝐷 ∈ V
28	1 21	odubas	⊢ ( Base ‘ 𝑂 ) = ( Base ‘ 𝐷 )
29	1 22	oduleval	⊢ ◡ ( le ‘ 𝑂 ) = ( le ‘ 𝐷 )
30		eqid	⊢ ( lub ‘ 𝐷 ) = ( lub ‘ 𝐷 )
31		biid	⊢ ( ( ∀ 𝑐 ∈ 𝑎 𝑐 ◡ ( le ‘ 𝑂 ) 𝑏 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑐 ◡ ( le ‘ 𝑂 ) 𝑑 → 𝑏 ◡ ( le ‘ 𝑂 ) 𝑑 ) ) ↔ ( ∀ 𝑐 ∈ 𝑎 𝑐 ◡ ( le ‘ 𝑂 ) 𝑏 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑐 ◡ ( le ‘ 𝑂 ) 𝑑 → 𝑏 ◡ ( le ‘ 𝑂 ) 𝑑 ) ) )
32		id	⊢ ( 𝐷 ∈ V → 𝐷 ∈ V )
33	28 29 30 31 32	lubfval	⊢ ( 𝐷 ∈ V → ( lub ‘ 𝐷 ) = ( ( 𝑎 ∈ 𝒫 ( Base ‘ 𝑂 ) ↦ ( ℩ 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑐 ◡ ( le ‘ 𝑂 ) 𝑏 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑐 ◡ ( le ‘ 𝑂 ) 𝑑 → 𝑏 ◡ ( le ‘ 𝑂 ) 𝑑 ) ) ) ) ↾ { 𝑎 ∣ ∃! 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑐 ◡ ( le ‘ 𝑂 ) 𝑏 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑐 ◡ ( le ‘ 𝑂 ) 𝑑 → 𝑏 ◡ ( le ‘ 𝑂 ) 𝑑 ) ) } ) )
34	27 33	mp1i	⊢ ( 𝑂 ∈ 𝑉 → ( lub ‘ 𝐷 ) = ( ( 𝑎 ∈ 𝒫 ( Base ‘ 𝑂 ) ↦ ( ℩ 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑐 ◡ ( le ‘ 𝑂 ) 𝑏 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑐 ◡ ( le ‘ 𝑂 ) 𝑑 → 𝑏 ◡ ( le ‘ 𝑂 ) 𝑑 ) ) ) ) ↾ { 𝑎 ∣ ∃! 𝑏 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑐 ◡ ( le ‘ 𝑂 ) 𝑏 ∧ ∀ 𝑑 ∈ ( Base ‘ 𝑂 ) ( ∀ 𝑐 ∈ 𝑎 𝑐 ◡ ( le ‘ 𝑂 ) 𝑑 → 𝑏 ◡ ( le ‘ 𝑂 ) 𝑑 ) ) } ) )
35	20 26 34	3eqtr4a	⊢ ( 𝑂 ∈ 𝑉 → ( glb ‘ 𝑂 ) = ( lub ‘ 𝐷 ) )
36	2 35	syl5eq	⊢ ( 𝑂 ∈ 𝑉 → 𝐿 = ( lub ‘ 𝐷 ) )