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	|- B = ( Base ` K )
	ple1.u	|- U = ( lub ` K )
	ple1.l	|- .<_ = ( le ` K )
	ple1.1	|- .1. = ( 1. ` K )
	ple1.k	|- ( ph -> K e. V )
	ple1.x	|- ( ph -> X e. B )
	ple1.d	|- ( ph -> B e. dom U )
Assertion	ple1	|- ( ph -> X .<_ .1. )

Proof

Step	Hyp	Ref	Expression
1		ple1.b	|- B = ( Base ` K )
2		ple1.u	|- U = ( lub ` K )
3		ple1.l	|- .<_ = ( le ` K )
4		ple1.1	|- .1. = ( 1. ` K )
5		ple1.k	|- ( ph -> K e. V )
6		ple1.x	|- ( ph -> X e. B )
7		ple1.d	|- ( ph -> B e. dom U )
8	1 3 2 5 7 6	luble	|- ( ph -> X .<_ ( U ` B ) )
9	1 2 4	p1val	|- ( K e. V -> .1. = ( U ` B ) )
10	5 9	syl	|- ( ph -> .1. = ( U ` B ) )
11	8 10	breqtrrd	|- ( ph -> X .<_ .1. )