# Metamath Proof Explorer

## Theorem poslubdg

Description: Properties which determine the least upper bound in a poset. (Contributed by Stefan O'Rear, 31-Jan-2015)

Ref Expression
Hypotheses poslubdg.l
poslubdg.b ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{K}}$
poslubdg.u ${⊢}{\phi }\to {U}=\mathrm{lub}\left({K}\right)$
poslubdg.k ${⊢}{\phi }\to {K}\in \mathrm{Poset}$
poslubdg.s ${⊢}{\phi }\to {S}\subseteq {B}$
poslubdg.t ${⊢}{\phi }\to {T}\in {B}$
poslubdg.ub
poslubdg.le
Assertion poslubdg ${⊢}{\phi }\to {U}\left({S}\right)={T}$

### Proof

Step Hyp Ref Expression
1 poslubdg.l
2 poslubdg.b ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{K}}$
3 poslubdg.u ${⊢}{\phi }\to {U}=\mathrm{lub}\left({K}\right)$
4 poslubdg.k ${⊢}{\phi }\to {K}\in \mathrm{Poset}$
5 poslubdg.s ${⊢}{\phi }\to {S}\subseteq {B}$
6 poslubdg.t ${⊢}{\phi }\to {T}\in {B}$
7 poslubdg.ub
8 poslubdg.le
9 3 fveq1d ${⊢}{\phi }\to {U}\left({S}\right)=\mathrm{lub}\left({K}\right)\left({S}\right)$
10 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
11 eqid ${⊢}\mathrm{lub}\left({K}\right)=\mathrm{lub}\left({K}\right)$
12 5 2 sseqtrd ${⊢}{\phi }\to {S}\subseteq {\mathrm{Base}}_{{K}}$
13 6 2 eleqtrd ${⊢}{\phi }\to {T}\in {\mathrm{Base}}_{{K}}$
14 2 eleq2d ${⊢}{\phi }\to \left({y}\in {B}↔{y}\in {\mathrm{Base}}_{{K}}\right)$
15 14 biimpar ${⊢}\left({\phi }\wedge {y}\in {\mathrm{Base}}_{{K}}\right)\to {y}\in {B}$
18 1 10 11 4 12 13 7 17 poslubd ${⊢}{\phi }\to \mathrm{lub}\left({K}\right)\left({S}\right)={T}$
19 9 18 eqtrd ${⊢}{\phi }\to {U}\left({S}\right)={T}$