Theorem lublecl

Description: The set of all elements less than a given element has an LUB. (Contributed by NM, 8-Sep-2018)

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

Proof

Step	Hyp	Ref	Expression
1		lublecl.b	|- B = ( Base ` K )
2		lublecl.l	|- .<_ = ( le ` K )
3		lublecl.u	|- U = ( lub ` K )
4		lublecl.k	|- ( ph -> K e. Poset )
5		lublecl.x	|- ( ph -> X e. B )
6		ssrab2	|- { y e. B | y .<_ X } C_ B
7	6	a1i	|- ( ph -> { y e. B | y .<_ X } C_ B )
8	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 ) )
9	8	ralrimiva	|- ( ph -> A. 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 ) )
10		reu6i	|- ( ( X e. B /\ A. 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 ) ) -> E! 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 ) ) )
11	5 9 10	syl2anc	|- ( ph -> E! 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 ) ) )
12		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 ) ) )
13	1 2 3 12 4	lubeldm	|- ( ph -> ( { y e. B | y .<_ X } e. dom U <-> ( { y e. B | y .<_ X } C_ B /\ E! 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 ) ) ) ) )
14	7 11 13	mpbir2and	|- ( ph -> { y e. B | y .<_ X } e. dom U )