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 -1 c ↔ c ≤ O b
6 5 ralbii ⊢ ∀ c ∈ a b ≤ O -1 c ↔ ∀ c ∈ a c ≤ O b
7 vex ⊢ d ∈ V
8 7 4 brcnv ⊢ d ≤ O -1 c ↔ c ≤ O d
9 8 ralbii ⊢ ∀ c ∈ a d ≤ O -1 c ↔ ∀ c ∈ a c ≤ O d
10 7 3 brcnv ⊢ d ≤ O -1 b ↔ b ≤ O d
11 9 10 imbi12i ⊢ ∀ c ∈ a d ≤ O -1 c → d ≤ O -1 b ↔ ∀ c ∈ a c ≤ O d → b ≤ O d
12 11 ralbii ⊢ ∀ d ∈ Base O ∀ c ∈ a d ≤ O -1 c → d ≤ O -1 b ↔ ∀ d ∈ Base O ∀ c ∈ a c ≤ O d → b ≤ O d
13 6 12 anbi12i ⊢ ∀ c ∈ a b ≤ O -1 c ∧ ∀ d ∈ Base O ∀ c ∈ a d ≤ O -1 c → d ≤ O -1 b ↔ ∀ c ∈ a c ≤ O b ∧ ∀ d ∈ Base O ∀ c ∈ a c ≤ O d → b ≤ O d
14 13 a1i ⊢ b ∈ Base O → ∀ c ∈ a b ≤ O -1 c ∧ ∀ d ∈ Base O ∀ c ∈ a d ≤ O -1 c → d ≤ O -1 b ↔ ∀ c ∈ a c ≤ O b ∧ ∀ d ∈ Base O ∀ c ∈ a c ≤ O d → b ≤ O d
15 14 riotabiia ⊢ ι b ∈ Base O | ∀ c ∈ a b ≤ O -1 c ∧ ∀ d ∈ Base O ∀ c ∈ a d ≤ O -1 c → d ≤ O -1 b = ι b ∈ Base O | ∀ c ∈ a c ≤ O b ∧ ∀ d ∈ Base O ∀ c ∈ a c ≤ O d → b ≤ O d
16 15 mpteq2i ⊢ a ∈ 𝒫 Base O ⟼ ι b ∈ Base O | ∀ c ∈ a b ≤ O -1 c ∧ ∀ d ∈ Base O ∀ c ∈ a d ≤ O -1 c → d ≤ O -1 b = a ∈ 𝒫 Base O ⟼ ι b ∈ Base O | ∀ c ∈ a c ≤ O b ∧ ∀ d ∈ Base O ∀ c ∈ a c ≤ O d → b ≤ O d
17 13 reubii ⊢ ∃! b ∈ Base O ∀ c ∈ a b ≤ O -1 c ∧ ∀ d ∈ Base O ∀ c ∈ a d ≤ O -1 c → d ≤ O -1 b ↔ ∃! b ∈ Base O ∀ c ∈ a c ≤ O b ∧ ∀ d ∈ Base O ∀ c ∈ a c ≤ O d → b ≤ O d
18 17 abbii ⊢ a | ∃! b ∈ Base O ∀ c ∈ a b ≤ O -1 c ∧ ∀ d ∈ Base O ∀ c ∈ a d ≤ O -1 c → d ≤ O -1 b = a | ∃! b ∈ Base O ∀ c ∈ a c ≤ O b ∧ ∀ d ∈ Base O ∀ c ∈ a c ≤ O d → b ≤ O d
19 16 18 reseq12i ⊢ a ∈ 𝒫 Base O ⟼ ι b ∈ Base O | ∀ c ∈ a b ≤ O -1 c ∧ ∀ d ∈ Base O ∀ c ∈ a d ≤ O -1 c → d ≤ O -1 b ↾ a | ∃! b ∈ Base O ∀ c ∈ a b ≤ O -1 c ∧ ∀ d ∈ Base O ∀ c ∈ a d ≤ O -1 c → d ≤ O -1 b = a ∈ 𝒫 Base O ⟼ ι b ∈ Base O | ∀ c ∈ a c ≤ O b ∧ ∀ d ∈ Base O ∀ c ∈ a c ≤ O d → b ≤ O d ↾ a | ∃! b ∈ Base O ∀ c ∈ a c ≤ O b ∧ ∀ d ∈ Base O ∀ c ∈ a c ≤ O d → b ≤ O d
20 19 eqcomi ⊢ a ∈ 𝒫 Base O ⟼ ι b ∈ Base O | ∀ c ∈ a c ≤ O b ∧ ∀ d ∈ Base O ∀ c ∈ a c ≤ O d → b ≤ O d ↾ a | ∃! b ∈ Base O ∀ c ∈ a c ≤ O b ∧ ∀ d ∈ Base O ∀ c ∈ a c ≤ O d → b ≤ O d = a ∈ 𝒫 Base O ⟼ ι b ∈ Base O | ∀ c ∈ a b ≤ O -1 c ∧ ∀ d ∈ Base O ∀ c ∈ a d ≤ O -1 c → d ≤ O -1 b ↾ a | ∃! b ∈ Base O ∀ c ∈ a b ≤ O -1 c ∧ ∀ d ∈ Base O ∀ c ∈ a d ≤ O -1 c → d ≤ O -1 b
21 eqid ⊢ Base O = Base O
22 eqid ⊢ ≤ O = ≤ O
23 eqid ⊢ lub ⁡ O = lub ⁡ O
24 biid ⊢ ∀ c ∈ a c ≤ O b ∧ ∀ d ∈ Base O ∀ c ∈ a c ≤ O d → b ≤ O d ↔ ∀ c ∈ a c ≤ O b ∧ ∀ d ∈ Base O ∀ c ∈ a c ≤ O d → b ≤ O d
25 id ⊢ O ∈ V → O ∈ V
26 21 22 23 24 25 lubfval ⊢ O ∈ V → lub ⁡ O = a ∈ 𝒫 Base O ⟼ ι b ∈ Base O | ∀ c ∈ a c ≤ O b ∧ ∀ d ∈ Base O ∀ c ∈ a c ≤ O d → b ≤ O d ↾ a | ∃! b ∈ Base O ∀ c ∈ a c ≤ O b ∧ ∀ d ∈ Base O ∀ c ∈ a c ≤ O d → b ≤ O d
27 1 fvexi ⊢ D ∈ V
28 1 21 odubas ⊢ Base O = Base D
29 1 22 oduleval ⊢ ≤ O -1 = ≤ D
30 eqid ⊢ glb ⁡ D = glb ⁡ D
31 biid ⊢ ∀ c ∈ a b ≤ O -1 c ∧ ∀ d ∈ Base O ∀ c ∈ a d ≤ O -1 c → d ≤ O -1 b ↔ ∀ c ∈ a b ≤ O -1 c ∧ ∀ d ∈ Base O ∀ c ∈ a d ≤ O -1 c → d ≤ O -1 b
32 id ⊢ D ∈ V → D ∈ V
33 28 29 30 31 32 glbfval ⊢ D ∈ V → glb ⁡ D = a ∈ 𝒫 Base O ⟼ ι b ∈ Base O | ∀ c ∈ a b ≤ O -1 c ∧ ∀ d ∈ Base O ∀ c ∈ a d ≤ O -1 c → d ≤ O -1 b ↾ a | ∃! b ∈ Base O ∀ c ∈ a b ≤ O -1 c ∧ ∀ d ∈ Base O ∀ c ∈ a d ≤ O -1 c → d ≤ O -1 b
34 27 33 mp1i ⊢ O ∈ V → glb ⁡ D = a ∈ 𝒫 Base O ⟼ ι b ∈ Base O | ∀ c ∈ a b ≤ O -1 c ∧ ∀ d ∈ Base O ∀ c ∈ a d ≤ O -1 c → d ≤ O -1 b ↾ a | ∃! b ∈ Base O ∀ c ∈ a b ≤ O -1 c ∧ ∀ d ∈ Base O ∀ c ∈ a d ≤ O -1 c → d ≤ O -1 b
35 20 26 34 3eqtr4a ⊢ O ∈ V → lub ⁡ O = glb ⁡ D
36 2 35 syl5eq ⊢ O ∈ V → U = glb ⁡ D