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 𝐵 = ( Base ‘ 𝐾 )
ple1.u 𝑈 = ( lub ‘ 𝐾 )
ple1.l = ( le ‘ 𝐾 )
ple1.1 1 = ( 1. ‘ 𝐾 )
ple1.k ( 𝜑𝐾𝑉 )
ple1.x ( 𝜑𝑋𝐵 )
ple1.d ( 𝜑𝐵 ∈ dom 𝑈 )
Assertion ple1 ( 𝜑𝑋 1 )

Proof

Step Hyp Ref Expression
1 ple1.b 𝐵 = ( Base ‘ 𝐾 )
2 ple1.u 𝑈 = ( lub ‘ 𝐾 )
3 ple1.l = ( le ‘ 𝐾 )
4 ple1.1 1 = ( 1. ‘ 𝐾 )
5 ple1.k ( 𝜑𝐾𝑉 )
6 ple1.x ( 𝜑𝑋𝐵 )
7 ple1.d ( 𝜑𝐵 ∈ dom 𝑈 )
8 1 3 2 5 7 6 luble ( 𝜑𝑋 ( 𝑈𝐵 ) )
9 1 2 4 p1val ( 𝐾𝑉1 = ( 𝑈𝐵 ) )
10 5 9 syl ( 𝜑1 = ( 𝑈𝐵 ) )
11 8 10 breqtrrd ( 𝜑𝑋 1 )