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 ) |
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 ) |