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={\mathrm{Base}}_K$$
	lublecl.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	lublecl.u	$$⊢U=\mathrm{lub}\left(K\right)$$
	lublecl.k	$$⊢\phi \to K\in \mathrm{Poset}$$
	lublecl.x	$$⊢\phi \to X\in B$$
Assertion	lublecl	$$⊢\phi \to \left\{y\in B|y\underset{\dot{}}{\le }X\right\}\in \mathrm{dom}U$$

Proof

Step	Hyp	Ref	Expression
1		lublecl.b	$$⊢B={\mathrm{Base}}_K$$
2		lublecl.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		lublecl.u	$$⊢U=\mathrm{lub}\left(K\right)$$
4		lublecl.k	$$⊢\phi \to K\in \mathrm{Poset}$$
5		lublecl.x	$$⊢\phi \to X\in B$$
6		ssrab2	$$⊢\left\{y\in B|y\underset{\dot{}}{\le }X\right\}\subseteq B$$
7	6	a1i	$$⊢\phi \to \left\{y\in B|y\underset{\dot{}}{\le }X\right\}\subseteq B$$
8	1 2 3 4 5	lublecllem	$$⊢\left(\phi \wedge x\in B\right)\to \left(\left(\forall z\in \left\{y\in B|y\underset{\dot{}}{\le }X\right\}z\underset{\dot{}}{\le }x\wedge \forall w\in B\left(\forall z\in \left\{y\in B|y\underset{\dot{}}{\le }X\right\}z\underset{\dot{}}{\le }w\to x\underset{\dot{}}{\le }w\right)\right)\leftrightarrow x=X\right)$$
9	8	ralrimiva	$$⊢\phi \to \forall x\in B\left(\left(\forall z\in \left\{y\in B|y\underset{\dot{}}{\le }X\right\}z\underset{\dot{}}{\le }x\wedge \forall w\in B\left(\forall z\in \left\{y\in B|y\underset{\dot{}}{\le }X\right\}z\underset{\dot{}}{\le }w\to x\underset{\dot{}}{\le }w\right)\right)\leftrightarrow x=X\right)$$
10		reu6i	$$⊢\left(X\in B\wedge \forall x\in B\left(\left(\forall z\in \left\{y\in B|y\underset{\dot{}}{\le }X\right\}z\underset{\dot{}}{\le }x\wedge \forall w\in B\left(\forall z\in \left\{y\in B|y\underset{\dot{}}{\le }X\right\}z\underset{\dot{}}{\le }w\to x\underset{\dot{}}{\le }w\right)\right)\leftrightarrow x=X\right)\right)\to \exists !x\in B\left(\forall z\in \left\{y\in B|y\underset{\dot{}}{\le }X\right\}z\underset{\dot{}}{\le }x\wedge \forall w\in B\left(\forall z\in \left\{y\in B|y\underset{\dot{}}{\le }X\right\}z\underset{\dot{}}{\le }w\to x\underset{\dot{}}{\le }w\right)\right)$$
11	5 9 10	syl2anc	$$⊢\phi \to \exists !x\in B\left(\forall z\in \left\{y\in B|y\underset{\dot{}}{\le }X\right\}z\underset{\dot{}}{\le }x\wedge \forall w\in B\left(\forall z\in \left\{y\in B|y\underset{\dot{}}{\le }X\right\}z\underset{\dot{}}{\le }w\to x\underset{\dot{}}{\le }w\right)\right)$$
12		biid	$$⊢\left(\forall z\in \left\{y\in B|y\underset{\dot{}}{\le }X\right\}z\underset{\dot{}}{\le }x\wedge \forall w\in B\left(\forall z\in \left\{y\in B|y\underset{\dot{}}{\le }X\right\}z\underset{\dot{}}{\le }w\to x\underset{\dot{}}{\le }w\right)\right)\leftrightarrow \left(\forall z\in \left\{y\in B|y\underset{\dot{}}{\le }X\right\}z\underset{\dot{}}{\le }x\wedge \forall w\in B\left(\forall z\in \left\{y\in B|y\underset{\dot{}}{\le }X\right\}z\underset{\dot{}}{\le }w\to x\underset{\dot{}}{\le }w\right)\right)$$
13	1 2 3 12 4	lubeldm	$$⊢\phi \to \left(\left\{y\in B|y\underset{\dot{}}{\le }X\right\}\in \mathrm{dom}U\leftrightarrow \left(\left\{y\in B|y\underset{\dot{}}{\le }X\right\}\subseteq B\wedge \exists !x\in B\left(\forall z\in \left\{y\in B|y\underset{\dot{}}{\le }X\right\}z\underset{\dot{}}{\le }x\wedge \forall w\in B\left(\forall z\in \left\{y\in B|y\underset{\dot{}}{\le }X\right\}z\underset{\dot{}}{\le }w\to x\underset{\dot{}}{\le }w\right)\right)\right)\right)$$
14	7 11 13	mpbir2and	$$⊢\phi \to \left\{y\in B|y\underset{\dot{}}{\le }X\right\}\in \mathrm{dom}U$$