# 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}={\mathrm{Base}}_{{K}}$
toslub.l
toslub.1 ${⊢}{\phi }\to {K}\in \mathrm{Toset}$
toslub.2 ${⊢}{\phi }\to {A}\subseteq {B}$
Assertion toslub

### Proof

Step Hyp Ref Expression
1 toslub.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 toslub.l
3 toslub.1 ${⊢}{\phi }\to {K}\in \mathrm{Toset}$
4 toslub.2 ${⊢}{\phi }\to {A}\subseteq {B}$
5 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
6 1 2 3 4 5 toslublem
7 6 riotabidva
8 eqid ${⊢}\mathrm{lub}\left({K}\right)=\mathrm{lub}\left({K}\right)$
9 biid ${⊢}\left(\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}{b}{\le }_{{K}}{a}\wedge \forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}{b}{\le }_{{K}}{c}\to {a}{\le }_{{K}}{c}\right)\right)↔\left(\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}{b}{\le }_{{K}}{a}\wedge \forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}{b}{\le }_{{K}}{c}\to {a}{\le }_{{K}}{c}\right)\right)$
10 1 5 8 9 3 4 lubval ${⊢}{\phi }\to \mathrm{lub}\left({K}\right)\left({A}\right)=\left(\iota {a}\in {B}|\left(\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}{b}{\le }_{{K}}{a}\wedge \forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}{b}{\le }_{{K}}{c}\to {a}{\le }_{{K}}{c}\right)\right)\right)$
11 1 5 2 tosso
12 11 ibi
13 12 simpld
14 id
15 14 supval2
16 3 13 15 3syl
17 7 10 16 3eqtr4d