This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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