Theorem lubprdm

Description: The set of two comparable elements in a poset has LUB. (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\}$$
	lubpr.u	$$⊢U=\mathrm{lub}\left(K\right)$$
Assertion	lubprdm	$$⊢\phi \to S\in \mathrm{dom}U$$

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		lubpr.u	$$⊢U=\mathrm{lub}\left(K\right)$$
9	1 2 3 4 5 6 7 8	lubprlem	$$⊢\phi \to \left(S\in \mathrm{dom}U\wedge U\left(S\right)=Y\right)$$
10	9	simpld	$$⊢\phi \to S\in \mathrm{dom}U$$