Metamath Proof Explorer

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 ⊢D=ODual⁡O
odulub.l ⊢L=glb⁡O
Assertion odulub ⊢O∈V→L=lub⁡D

Proof

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