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 | ple1.b | |- B = ( Base ` K ) |
|
ple1.u | |- U = ( lub ` K ) |
||
ple1.l | |- .<_ = ( le ` K ) |
||
ple1.1 | |- .1. = ( 1. ` K ) |
||
ple1.k | |- ( ph -> K e. V ) |
||
ple1.x | |- ( ph -> X e. B ) |
||
ple1.d | |- ( ph -> B e. dom U ) |
||
Assertion | ple1 | |- ( ph -> X .<_ .1. ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ple1.b | |- B = ( Base ` K ) |
|
2 | ple1.u | |- U = ( lub ` K ) |
|
3 | ple1.l | |- .<_ = ( le ` K ) |
|
4 | ple1.1 | |- .1. = ( 1. ` K ) |
|
5 | ple1.k | |- ( ph -> K e. V ) |
|
6 | ple1.x | |- ( ph -> X e. B ) |
|
7 | ple1.d | |- ( ph -> B e. dom U ) |
|
8 | 1 3 2 5 7 6 | luble | |- ( ph -> X .<_ ( U ` B ) ) |
9 | 1 2 4 | p1val | |- ( K e. V -> .1. = ( U ` B ) ) |
10 | 5 9 | syl | |- ( ph -> .1. = ( U ` B ) ) |
11 | 8 10 | breqtrrd | |- ( ph -> X .<_ .1. ) |