Theorem glble

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

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

Proof

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