Theorem lubid

Description: The LUB of elements less than or equal to a fixed value equals that value. (Contributed by NM, 19-Oct-2011) (Revised by NM, 7-Sep-2018)

	Ref	Expression
Hypotheses	lubid.b	|- B = ( Base ` K )
	lubid.l	|- .<_ = ( le ` K )
	lubid.u	|- U = ( lub ` K )
	lubid.k	|- ( ph -> K e. Poset )
	lubid.x	|- ( ph -> X e. B )
Assertion	lubid	|- ( ph -> ( U ` { y e. B | y .<_ X } ) = X )

Proof

Step	Hyp	Ref	Expression
1		lubid.b	|- B = ( Base ` K )
2		lubid.l	|- .<_ = ( le ` K )
3		lubid.u	|- U = ( lub ` K )
4		lubid.k	|- ( ph -> K e. Poset )
5		lubid.x	|- ( ph -> X e. B )
6		biid	|- ( ( A. z e. { y e. B | y .<_ X } z .<_ x /\ A. w e. B ( A. z e. { y e. B | y .<_ X } z .<_ w -> x .<_ w ) ) <-> ( A. z e. { y e. B | y .<_ X } z .<_ x /\ A. w e. B ( A. z e. { y e. B | y .<_ X } z .<_ w -> x .<_ w ) ) )
7		ssrab2	|- { y e. B | y .<_ X } C_ B
8	7	a1i	|- ( ph -> { y e. B | y .<_ X } C_ B )
9	1 2 3 6 4 8	lubval	|- ( ph -> ( U ` { y e. B | y .<_ X } ) = ( iota_ x e. B ( A. z e. { y e. B | y .<_ X } z .<_ x /\ A. w e. B ( A. z e. { y e. B | y .<_ X } z .<_ w -> x .<_ w ) ) ) )
10	1 2 3 4 5	lublecllem	|- ( ( ph /\ x e. B ) -> ( ( A. z e. { y e. B | y .<_ X } z .<_ x /\ A. w e. B ( A. z e. { y e. B | y .<_ X } z .<_ w -> x .<_ w ) ) <-> x = X ) )
11	5 10	riota5	|- ( ph -> ( iota_ x e. B ( A. z e. { y e. B | y .<_ X } z .<_ x /\ A. w e. B ( A. z e. { y e. B | y .<_ X } z .<_ w -> x .<_ w ) ) ) = X )
12	9 11	eqtrd	|- ( ph -> ( U ` { y e. B | y .<_ X } ) = X )