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