Metamath Proof Explorer

Theorem toslub

Description: In a toset, the lowest upper bound lub , defined for partial orders is the supremum, sup ( A , B , .< ) , defined for total orders. (these are the set.mm definitions: lowest upper bound and supremum are normally synonymous). Note that those two values are also equal if such a supremum does not exist: in that case, both are equal to the empty set. (Contributed by Thierry Arnoux, 15-Feb-2018) (Revised by Thierry Arnoux, 24-Sep-2018)

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

Proof

Step Hyp Ref Expression
1 toslub.b ⊢ B = Base K
2 toslub.l ⊢ < ˙ = < K
3 toslub.1 ⊢ φ → K ∈ Toset
4 toslub.2 ⊢ φ → A ⊆ B
5 eqid ⊢ ≤ K = ≤ K
6 1 2 3 4 5 toslublem ⊢ φ ∧ a ∈ B → ∀ b ∈ A b ≤ K a ∧ ∀ c ∈ B ∀ b ∈ A b ≤ K c → a ≤ K c ↔ ∀ b ∈ A ¬ a < ˙ b ∧ ∀ b ∈ B b < ˙ a → ∃ d ∈ A b < ˙ d
7 6 riotabidva ⊢ φ → ι a ∈ B | ∀ b ∈ A b ≤ K a ∧ ∀ c ∈ B ∀ b ∈ A b ≤ K c → a ≤ K c = ι a ∈ B | ∀ b ∈ A ¬ a < ˙ b ∧ ∀ b ∈ B b < ˙ a → ∃ d ∈ A b < ˙ d
8 eqid ⊢ lub ⁡ K = lub ⁡ K
9 biid ⊢ ∀ b ∈ A b ≤ K a ∧ ∀ c ∈ B ∀ b ∈ A b ≤ K c → a ≤ K c ↔ ∀ b ∈ A b ≤ K a ∧ ∀ c ∈ B ∀ b ∈ A b ≤ K c → a ≤ K c
10 1 5 8 9 3 4 lubval ⊢ φ → lub ⁡ K ⁡ A = ι a ∈ B | ∀ b ∈ A b ≤ K a ∧ ∀ c ∈ B ∀ b ∈ A b ≤ K c → a ≤ K c
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 id ⊢ < ˙ Or B → < ˙ Or B
15 14 supval2 ⊢ < ˙ Or B → sup A B < ˙ = ι a ∈ B | ∀ b ∈ A ¬ a < ˙ b ∧ ∀ b ∈ B b < ˙ a → ∃ d ∈ A b < ˙ d
16 3 13 15 3syl ⊢ φ → sup A B < ˙ = ι a ∈ B | ∀ b ∈ A ¬ a < ˙ b ∧ ∀ b ∈ B b < ˙ a → ∃ d ∈ A b < ˙ d
17 7 10 16 3eqtr4d ⊢ φ → lub ⁡ K ⁡ A = sup A B < ˙