# 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
`|- .<_ = ( le ` K )`
poslubdg.b
`|- ( ph -> B = ( Base ` K ) )`
poslubdg.u
`|- ( ph -> U = ( lub ` K ) )`
poslubdg.k
`|- ( ph -> K e. Poset )`
poslubdg.s
`|- ( ph -> S C_ B )`
poslubdg.t
`|- ( ph -> T e. B )`
poslubdg.ub
`|- ( ( ph /\ x e. S ) -> x .<_ T )`
poslubdg.le
`|- ( ( ph /\ y e. B /\ A. x e. S x .<_ y ) -> T .<_ y )`
Assertion poslubdg
`|- ( ph -> ( U ` S ) = T )`

### Proof

Step Hyp Ref Expression
1 poslubdg.l
` |-  .<_ = ( le ` K )`
2 poslubdg.b
` |-  ( ph -> B = ( Base ` K ) )`
3 poslubdg.u
` |-  ( ph -> U = ( lub ` K ) )`
4 poslubdg.k
` |-  ( ph -> K e. Poset )`
5 poslubdg.s
` |-  ( ph -> S C_ B )`
6 poslubdg.t
` |-  ( ph -> T e. B )`
7 poslubdg.ub
` |-  ( ( ph /\ x e. S ) -> x .<_ T )`
8 poslubdg.le
` |-  ( ( ph /\ y e. B /\ A. x e. S x .<_ y ) -> T .<_ y )`
9 3 fveq1d
` |-  ( ph -> ( U ` S ) = ( ( lub ` K ) ` S ) )`
10 eqid
` |-  ( Base ` K ) = ( Base ` K )`
11 eqid
` |-  ( lub ` K ) = ( lub ` K )`
12 5 2 sseqtrd
` |-  ( ph -> S C_ ( Base ` K ) )`
13 6 2 eleqtrd
` |-  ( ph -> T e. ( Base ` K ) )`
14 2 eleq2d
` |-  ( ph -> ( y e. B <-> y e. ( Base ` K ) ) )`
15 14 biimpar
` |-  ( ( ph /\ y e. ( Base ` K ) ) -> y e. B )`
` |-  ( ( ph /\ y e. ( Base ` K ) /\ A. x e. S x .<_ y ) -> y e. B )`
` |-  ( ( ph /\ y e. ( Base ` K ) /\ A. x e. S x .<_ y ) -> T .<_ y )`
` |-  ( ph -> ( ( lub ` K ) ` S ) = T )`
` |-  ( ph -> ( U ` S ) = T )`