Metamath Proof Explorer

Theorem tosglb

Description: Same theorem as toslub , for infinimum. (Contributed by Thierry Arnoux, 17-Feb-2018) (Revised by AV, 28-Sep-2020)

Ref Expression
Hypotheses tosglb.b ⊢ B = Base K
tosglb.l ⊢ < ˙ = < K
tosglb.1 ⊢ φ → K ∈ Toset
tosglb.2 ⊢ φ → A ⊆ B
Assertion tosglb ⊢ φ → glb ⁡ K ⁡ A = sup A B < ˙

Proof

Step Hyp Ref Expression
1 tosglb.b ⊢ B = Base K
2 tosglb.l ⊢ < ˙ = < K
3 tosglb.1 ⊢ φ → K ∈ Toset
4 tosglb.2 ⊢ φ → A ⊆ B
5 eqid ⊢ ≤ K = ≤ K
6 1 2 3 4 5 tosglblem ⊢ φ ∧ a ∈ B → ∀ b ∈ A a ≤ K b ∧ ∀ c ∈ B ∀ b ∈ A c ≤ K b → c ≤ K a ↔ ∀ b ∈ A ¬ a < ˙ -1 b ∧ ∀ b ∈ B b < ˙ -1 a → ∃ d ∈ A b < ˙ -1 d
7 6 riotabidva ⊢ φ → ι a ∈ B | ∀ b ∈ A a ≤ K b ∧ ∀ c ∈ B ∀ b ∈ A c ≤ K b → c ≤ K a = ι a ∈ B | ∀ b ∈ A ¬ a < ˙ -1 b ∧ ∀ b ∈ B b < ˙ -1 a → ∃ d ∈ A b < ˙ -1 d
8 eqid ⊢ glb ⁡ K = glb ⁡ K
9 biid ⊢ ∀ b ∈ A a ≤ K b ∧ ∀ c ∈ B ∀ b ∈ A c ≤ K b → c ≤ K a ↔ ∀ b ∈ A a ≤ K b ∧ ∀ c ∈ B ∀ b ∈ A c ≤ K b → c ≤ K a
10 1 5 8 9 3 4 glbval ⊢ φ → glb ⁡ K ⁡ A = ι a ∈ B | ∀ b ∈ A a ≤ K b ∧ ∀ c ∈ B ∀ b ∈ A c ≤ K b → c ≤ K a
11 1 5 2 tosso ⊢ K ∈ Toset → K ∈ Toset ↔ < ˙ Or B ∧ I ↾ B ⊆ ≤ K
12 11 ibi ⊢ K ∈ Toset → < ˙ Or B ∧ I ↾ B ⊆ ≤ K
13 12 simpld ⊢ K ∈ Toset → < ˙ Or B
14 cnvso ⊢ < ˙ Or B ↔ < ˙ -1 Or B
15 13 14 sylib ⊢ K ∈ Toset → < ˙ -1 Or B
16 id ⊢ < ˙ -1 Or B → < ˙ -1 Or B
17 16 supval2 ⊢ < ˙ -1 Or B → sup A B < ˙ -1 = ι a ∈ B | ∀ b ∈ A ¬ a < ˙ -1 b ∧ ∀ b ∈ B b < ˙ -1 a → ∃ d ∈ A b < ˙ -1 d
18 3 15 17 3syl ⊢ φ → sup A B < ˙ -1 = ι a ∈ B | ∀ b ∈ A ¬ a < ˙ -1 b ∧ ∀ b ∈ B b < ˙ -1 a → ∃ d ∈ A b < ˙ -1 d
19 7 10 18 3eqtr4d ⊢ φ → glb ⁡ K ⁡ A = sup A B < ˙ -1
20 df-inf ⊢ sup A B < ˙ = sup A B < ˙ -1
21 20 eqcomi ⊢ sup A B < ˙ -1 = sup A B < ˙
22 21 a1i ⊢ φ → sup A B < ˙ -1 = sup A B < ˙
23 19 22 eqtrd ⊢ φ → glb ⁡ K ⁡ A = sup A B < ˙