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 𝐵 = ( Base ‘ 𝐾 )
p0le.g 𝐺 = ( glb ‘ 𝐾 )
p0le.l = ( le ‘ 𝐾 )
p0le.0 0 = ( 0. ‘ 𝐾 )
p0le.k ( 𝜑𝐾𝑉 )
p0le.x ( 𝜑𝑋𝐵 )
p0le.d ( 𝜑𝐵 ∈ dom 𝐺 )
Assertion p0le ( 𝜑0 𝑋 )

Proof

Step Hyp Ref Expression
1 p0le.b 𝐵 = ( Base ‘ 𝐾 )
2 p0le.g 𝐺 = ( glb ‘ 𝐾 )
3 p0le.l = ( le ‘ 𝐾 )
4 p0le.0 0 = ( 0. ‘ 𝐾 )
5 p0le.k ( 𝜑𝐾𝑉 )
6 p0le.x ( 𝜑𝑋𝐵 )
7 p0le.d ( 𝜑𝐵 ∈ dom 𝐺 )
8 1 2 4 p0val ( 𝐾𝑉0 = ( 𝐺𝐵 ) )
9 5 8 syl ( 𝜑0 = ( 𝐺𝐵 ) )
10 1 3 2 5 7 6 glble ( 𝜑 → ( 𝐺𝐵 ) 𝑋 )
11 9 10 eqbrtrd ( 𝜑0 𝑋 )