Metamath Proof Explorer


Theorem p0le

Description: Any element is less than or equal to a poset's upper bound (if defined). (Contributed by NM, 22-Oct-2011) (Revised by NM, 13-Sep-2018)

Ref Expression
Hypotheses p0le.b
|- B = ( Base ` K )
p0le.g
|- G = ( glb ` K )
p0le.l
|- .<_ = ( le ` K )
p0le.0
|- .0. = ( 0. ` K )
p0le.k
|- ( ph -> K e. V )
p0le.x
|- ( ph -> X e. B )
p0le.d
|- ( ph -> B e. dom G )
Assertion p0le
|- ( ph -> .0. .<_ X )

Proof

Step Hyp Ref Expression
1 p0le.b
 |-  B = ( Base ` K )
2 p0le.g
 |-  G = ( glb ` K )
3 p0le.l
 |-  .<_ = ( le ` K )
4 p0le.0
 |-  .0. = ( 0. ` K )
5 p0le.k
 |-  ( ph -> K e. V )
6 p0le.x
 |-  ( ph -> X e. B )
7 p0le.d
 |-  ( ph -> B e. dom G )
8 1 2 4 p0val
 |-  ( K e. V -> .0. = ( G ` B ) )
9 5 8 syl
 |-  ( ph -> .0. = ( G ` B ) )
10 1 3 2 5 7 6 glble
 |-  ( ph -> ( G ` B ) .<_ X )
11 9 10 eqbrtrd
 |-  ( ph -> .0. .<_ X )