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