# Metamath Proof Explorer

## Theorem poslubd

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

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

### Proof

Step Hyp Ref Expression
1 poslubd.l
2 poslubd.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
3 poslubd.u ${⊢}{U}=\mathrm{lub}\left({K}\right)$
4 poslubd.k ${⊢}{\phi }\to {K}\in \mathrm{Poset}$
5 poslubd.s ${⊢}{\phi }\to {S}\subseteq {B}$
6 poslubd.t ${⊢}{\phi }\to {T}\in {B}$
7 poslubd.ub
8 poslubd.le
9 biid
10 2 1 3 9 4 5 lubval
11 7 ralrimiva
12 8 3expia
13 12 ralrimiva
14 11 13 jca
15 breq2
16 15 ralbidv
17 breq1
18 17 imbi2d
19 18 ralbidv
20 16 19 anbi12d
21 20 rspcev
22 6 14 21 syl2anc
23 1 2 poslubmo
24 4 5 23 syl2anc
25 reu5
26 22 24 25 sylanbrc
27 20 riota2
28 6 26 27 syl2anc
29 14 28 mpbid
30 10 29 eqtrd ${⊢}{\phi }\to {U}\left({S}\right)={T}$