Theorem glbprdm

Description: The set of two comparable elements in a poset has GLB. (Contributed by Zhi Wang, 26-Sep-2024)

	Ref	Expression
Hypotheses	lubpr.k	$$⊢\phi \to K\in \mathrm{Poset}$$
	lubpr.b	$$⊢B={\mathrm{Base}}_K$$
	lubpr.x	$$⊢\phi \to X\in B$$
	lubpr.y	$$⊢\phi \to Y\in B$$
	lubpr.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	lubpr.c	$$⊢\phi \to X\underset{\dot{}}{\le }Y$$
	lubpr.s	$$⊢\phi \to S=\left\{X,Y\right\}$$
	glbpr.g	$$⊢G=\mathrm{glb}\left(K\right)$$
Assertion	glbprdm	$$⊢\phi \to S\in \mathrm{dom}G$$

Proof

Step	Hyp	Ref	Expression
1		lubpr.k	$$⊢\phi \to K\in \mathrm{Poset}$$
2		lubpr.b	$$⊢B={\mathrm{Base}}_K$$
3		lubpr.x	$$⊢\phi \to X\in B$$
4		lubpr.y	$$⊢\phi \to Y\in B$$
5		lubpr.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
6		lubpr.c	$$⊢\phi \to X\underset{\dot{}}{\le }Y$$
7		lubpr.s	$$⊢\phi \to S=\left\{X,Y\right\}$$
8		glbpr.g	$$⊢G=\mathrm{glb}\left(K\right)$$
9	1 2 3 4 5 6 7 8	glbprlem	$$⊢\phi \to \left(S\in \mathrm{dom}G\wedge G\left(S\right)=X\right)$$
10	9	simpld	$$⊢\phi \to S\in \mathrm{dom}G$$