Theorem luble

Description: The greatest lower bound is the least element. (Contributed by NM, 22-Oct-2011) (Revised by NM, 7-Sep-2018)

	Ref	Expression
Hypotheses	lubprop.b	$$⊢B={\mathrm{Base}}_K$$
	lubprop.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	lubprop.u	$$⊢U=\mathrm{lub}\left(K\right)$$
	lubprop.k	$$⊢\phi \to K\in V$$
	lubprop.s	$$⊢\phi \to S\in \mathrm{dom}U$$
	luble.x	$$⊢\phi \to X\in S$$
Assertion	luble	$$⊢\phi \to X\underset{\dot{}}{\le }U\left(S\right)$$

Proof

Step	Hyp	Ref	Expression
1		lubprop.b	$$⊢B={\mathrm{Base}}_K$$
2		lubprop.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		lubprop.u	$$⊢U=\mathrm{lub}\left(K\right)$$
4		lubprop.k	$$⊢\phi \to K\in V$$
5		lubprop.s	$$⊢\phi \to S\in \mathrm{dom}U$$
6		luble.x	$$⊢\phi \to X\in S$$
7		breq1	$$⊢y=X\to \left(y\underset{\dot{}}{\le }U\left(S\right)\leftrightarrow X\underset{\dot{}}{\le }U\left(S\right)\right)$$
8	1 2 3 4 5	lubprop	$$⊢\phi \to \left(\forall y\in Sy\underset{\dot{}}{\le }U\left(S\right)\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to U\left(S\right)\underset{\dot{}}{\le }z\right)\right)$$
9	8	simpld	$$⊢\phi \to \forall y\in Sy\underset{\dot{}}{\le }U\left(S\right)$$
10	7 9 6	rspcdva	$$⊢\phi \to X\underset{\dot{}}{\le }U\left(S\right)$$