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

Proof

Step	Hyp	Ref	Expression
1		lubid.b	$$⊢B={\mathrm{Base}}_K$$
2		lubid.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		lubid.u	$$⊢U=\mathrm{lub}\left(K\right)$$
4		lubid.k	$$⊢\phi \to K\in \mathrm{Poset}$$
5		lubid.x	$$⊢\phi \to X\in B$$
6		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)$$
7		ssrab2	$$⊢\left\{y\in B|y\underset{\dot{}}{\le }X\right\}\subseteq B$$
8	7	a1i	$$⊢\phi \to \left\{y\in B|y\underset{\dot{}}{\le }X\right\}\subseteq B$$
9	1 2 3 6 4 8	lubval	$$⊢\phi \to U\left(\left\{y\in B|y\underset{\dot{}}{\le }X\right\}\right)=\left(\iota 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)$$
10	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)$$
11	5 10	riota5	$$⊢\phi \to \left(\iota 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)=X$$
12	9 11	eqtrd	$$⊢\phi \to U\left(\left\{y\in B|y\underset{\dot{}}{\le }X\right\}\right)=X$$