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	|- B = ( Base ` K )
	p0le.g	|- G = ( glb ` K )
	p0le.l	|- .<_ = ( le ` K )
	p0le.0	|- .0. = ( 0. ` K )
	p0le.k	|- ( ph -> K e. V )
	p0le.x	|- ( ph -> X e. B )
	p0le.d	|- ( ph -> B e. dom G )
Assertion	p0le	|- ( ph -> .0. .<_ X )

Proof

Step	Hyp	Ref	Expression
1		p0le.b	|- B = ( Base ` K )
2		p0le.g	|- G = ( glb ` K )
3		p0le.l	|- .<_ = ( le ` K )
4		p0le.0	|- .0. = ( 0. ` K )
5		p0le.k	|- ( ph -> K e. V )
6		p0le.x	|- ( ph -> X e. B )
7		p0le.d	|- ( ph -> B e. dom G )
8	1 2 4	p0val	|- ( K e. V -> .0. = ( G ` B ) )
9	5 8	syl	|- ( ph -> .0. = ( G ` B ) )
10	1 3 2 5 7 6	glble	|- ( ph -> ( G ` B ) .<_ X )
11	9 10	eqbrtrd	|- ( ph -> .0. .<_ X )