Metamath Proof Explorer


Theorem ple1

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

Proof

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