Metamath Proof Explorer

Theorem oduglb

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

Ref Expression
Hypotheses oduglb.d ⊢D=ODual⁡O
oduglb.l ⊢U=lub⁡O
Assertion oduglb ⊢O∈V→U=glb⁡D

Proof

Step Hyp Ref Expression
1 oduglb.d ⊢D=ODual⁡O
2 oduglb.l ⊢U=lub⁡O
3 vex ⊢b∈V
4 vex ⊢c∈V
5 3 4 brcnv ⊢b≤O-1c↔c≤Ob
6 5 ralbii ⊢∀c∈ab≤O-1c↔∀c∈ac≤Ob
7 vex ⊢d∈V
8 7 4 brcnv ⊢d≤O-1c↔c≤Od
9 8 ralbii ⊢∀c∈ad≤O-1c↔∀c∈ac≤Od
10 7 3 brcnv ⊢d≤O-1b↔b≤Od
11 9 10 imbi12i ⊢∀c∈ad≤O-1c→d≤O-1b↔∀c∈ac≤Od→b≤Od
12 11 ralbii ⊢∀d∈BaseO∀c∈ad≤O-1c→d≤O-1b↔∀d∈BaseO∀c∈ac≤Od→b≤Od
13 6 12 anbi12i ⊢∀c∈ab≤O-1c∧∀d∈BaseO∀c∈ad≤O-1c→d≤O-1b↔∀c∈ac≤Ob∧∀d∈BaseO∀c∈ac≤Od→b≤Od
14 13 a1i ⊢b∈BaseO→∀c∈ab≤O-1c∧∀d∈BaseO∀c∈ad≤O-1c→d≤O-1b↔∀c∈ac≤Ob∧∀d∈BaseO∀c∈ac≤Od→b≤Od
15 14 riotabiia ⊢ιb∈BaseO|∀c∈ab≤O-1c∧∀d∈BaseO∀c∈ad≤O-1c→d≤O-1b=ιb∈BaseO|∀c∈ac≤Ob∧∀d∈BaseO∀c∈ac≤Od→b≤Od
16 15 mpteq2i ⊢a∈𝒫BaseO⟼ιb∈BaseO|∀c∈ab≤O-1c∧∀d∈BaseO∀c∈ad≤O-1c→d≤O-1b=a∈𝒫BaseO⟼ιb∈BaseO|∀c∈ac≤Ob∧∀d∈BaseO∀c∈ac≤Od→b≤Od
17 13 reubii ⊢∃!b∈BaseO∀c∈ab≤O-1c∧∀d∈BaseO∀c∈ad≤O-1c→d≤O-1b↔∃!b∈BaseO∀c∈ac≤Ob∧∀d∈BaseO∀c∈ac≤Od→b≤Od
18 17 abbii ⊢a|∃!b∈BaseO∀c∈ab≤O-1c∧∀d∈BaseO∀c∈ad≤O-1c→d≤O-1b=a|∃!b∈BaseO∀c∈ac≤Ob∧∀d∈BaseO∀c∈ac≤Od→b≤Od
19 16 18 reseq12i ⊢a∈𝒫BaseO⟼ιb∈BaseO|∀c∈ab≤O-1c∧∀d∈BaseO∀c∈ad≤O-1c→d≤O-1b↾a|∃!b∈BaseO∀c∈ab≤O-1c∧∀d∈BaseO∀c∈ad≤O-1c→d≤O-1b=a∈𝒫BaseO⟼ιb∈BaseO|∀c∈ac≤Ob∧∀d∈BaseO∀c∈ac≤Od→b≤Od↾a|∃!b∈BaseO∀c∈ac≤Ob∧∀d∈BaseO∀c∈ac≤Od→b≤Od
20 19 eqcomi ⊢a∈𝒫BaseO⟼ιb∈BaseO|∀c∈ac≤Ob∧∀d∈BaseO∀c∈ac≤Od→b≤Od↾a|∃!b∈BaseO∀c∈ac≤Ob∧∀d∈BaseO∀c∈ac≤Od→b≤Od=a∈𝒫BaseO⟼ιb∈BaseO|∀c∈ab≤O-1c∧∀d∈BaseO∀c∈ad≤O-1c→d≤O-1b↾a|∃!b∈BaseO∀c∈ab≤O-1c∧∀d∈BaseO∀c∈ad≤O-1c→d≤O-1b
21 eqid ⊢BaseO=BaseO
22 eqid ⊢≤O=≤O
23 eqid ⊢lub⁡O=lub⁡O
24 biid ⊢∀c∈ac≤Ob∧∀d∈BaseO∀c∈ac≤Od→b≤Od↔∀c∈ac≤Ob∧∀d∈BaseO∀c∈ac≤Od→b≤Od
25 id ⊢O∈V→O∈V
26 21 22 23 24 25 lubfval ⊢O∈V→lub⁡O=a∈𝒫BaseO⟼ιb∈BaseO|∀c∈ac≤Ob∧∀d∈BaseO∀c∈ac≤Od→b≤Od↾a|∃!b∈BaseO∀c∈ac≤Ob∧∀d∈BaseO∀c∈ac≤Od→b≤Od
27 1 fvexi ⊢D∈V
28 1 21 odubas ⊢BaseO=BaseD
29 1 22 oduleval ⊢≤O-1=≤D
30 eqid ⊢glb⁡D=glb⁡D
31 biid ⊢∀c∈ab≤O-1c∧∀d∈BaseO∀c∈ad≤O-1c→d≤O-1b↔∀c∈ab≤O-1c∧∀d∈BaseO∀c∈ad≤O-1c→d≤O-1b
32 id ⊢D∈V→D∈V
33 28 29 30 31 32 glbfval ⊢D∈V→glb⁡D=a∈𝒫BaseO⟼ιb∈BaseO|∀c∈ab≤O-1c∧∀d∈BaseO∀c∈ad≤O-1c→d≤O-1b↾a|∃!b∈BaseO∀c∈ab≤O-1c∧∀d∈BaseO∀c∈ad≤O-1c→d≤O-1b
34 27 33 mp1i ⊢O∈V→glb⁡D=a∈𝒫BaseO⟼ιb∈BaseO|∀c∈ab≤O-1c∧∀d∈BaseO∀c∈ad≤O-1c→d≤O-1b↾a|∃!b∈BaseO∀c∈ab≤O-1c∧∀d∈BaseO∀c∈ad≤O-1c→d≤O-1b
35 20 26 34 3eqtr4a ⊢O∈V→lub⁡O=glb⁡D
36 2 35 eqtrid ⊢O∈V→U=glb⁡D