Theorem poslubmo

Description: Least upper bounds in a poset are unique if they exist. (Contributed by Stefan O'Rear, 31-Jan-2015) (Revised by NM, 16-Jun-2017)

	Ref	Expression
Hypotheses	poslubmo.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	poslubmo.b	$$⊢B={\mathrm{Base}}_K$$
Assertion	poslubmo	$$⊢\left(K\in \mathrm{Poset}\wedge S\subseteq B\right)\to {\exists }^{*}x\in B\left(\forall y\in Sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		poslubmo.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		poslubmo.b	$$⊢B={\mathrm{Base}}_K$$
3		simprrl	$$⊢\left(\left(\left(K\in \mathrm{Poset}\wedge S\subseteq B\right)\wedge \left(x\in B\wedge w\in B\right)\right)\wedge \left(\left(\forall y\in Sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\wedge \left(\forall y\in Sy\underset{\dot{}}{\le }w\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to w\underset{\dot{}}{\le }z\right)\right)\right)\right)\to \forall y\in Sy\underset{\dot{}}{\le }w$$
4		breq2	$$⊢z=w\to \left(y\underset{\dot{}}{\le }z\leftrightarrow y\underset{\dot{}}{\le }w\right)$$
5	4	ralbidv	$$⊢z=w\to \left(\forall y\in Sy\underset{\dot{}}{\le }z\leftrightarrow \forall y\in Sy\underset{\dot{}}{\le }w\right)$$
6		breq2	$$⊢z=w\to \left(x\underset{\dot{}}{\le }z\leftrightarrow x\underset{\dot{}}{\le }w\right)$$
7	5 6	imbi12d	$$⊢z=w\to \left(\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\leftrightarrow \left(\forall y\in Sy\underset{\dot{}}{\le }w\to x\underset{\dot{}}{\le }w\right)\right)$$
8		simprlr	$$⊢\left(\left(\left(K\in \mathrm{Poset}\wedge S\subseteq B\right)\wedge \left(x\in B\wedge w\in B\right)\right)\wedge \left(\left(\forall y\in Sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\wedge \left(\forall y\in Sy\underset{\dot{}}{\le }w\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to w\underset{\dot{}}{\le }z\right)\right)\right)\right)\to \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)$$
9		simplrr	$$⊢\left(\left(\left(K\in \mathrm{Poset}\wedge S\subseteq B\right)\wedge \left(x\in B\wedge w\in B\right)\right)\wedge \left(\left(\forall y\in Sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\wedge \left(\forall y\in Sy\underset{\dot{}}{\le }w\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to w\underset{\dot{}}{\le }z\right)\right)\right)\right)\to w\in B$$
10	7 8 9	rspcdva	$$⊢\left(\left(\left(K\in \mathrm{Poset}\wedge S\subseteq B\right)\wedge \left(x\in B\wedge w\in B\right)\right)\wedge \left(\left(\forall y\in Sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\wedge \left(\forall y\in Sy\underset{\dot{}}{\le }w\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to w\underset{\dot{}}{\le }z\right)\right)\right)\right)\to \left(\forall y\in Sy\underset{\dot{}}{\le }w\to x\underset{\dot{}}{\le }w\right)$$
11	3 10	mpd	$$⊢\left(\left(\left(K\in \mathrm{Poset}\wedge S\subseteq B\right)\wedge \left(x\in B\wedge w\in B\right)\right)\wedge \left(\left(\forall y\in Sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\wedge \left(\forall y\in Sy\underset{\dot{}}{\le }w\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to w\underset{\dot{}}{\le }z\right)\right)\right)\right)\to x\underset{\dot{}}{\le }w$$
12		simprll	$$⊢\left(\left(\left(K\in \mathrm{Poset}\wedge S\subseteq B\right)\wedge \left(x\in B\wedge w\in B\right)\right)\wedge \left(\left(\forall y\in Sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\wedge \left(\forall y\in Sy\underset{\dot{}}{\le }w\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to w\underset{\dot{}}{\le }z\right)\right)\right)\right)\to \forall y\in Sy\underset{\dot{}}{\le }x$$
13		breq2	$$⊢z=x\to \left(y\underset{\dot{}}{\le }z\leftrightarrow y\underset{\dot{}}{\le }x\right)$$
14	13	ralbidv	$$⊢z=x\to \left(\forall y\in Sy\underset{\dot{}}{\le }z\leftrightarrow \forall y\in Sy\underset{\dot{}}{\le }x\right)$$
15		breq2	$$⊢z=x\to \left(w\underset{\dot{}}{\le }z\leftrightarrow w\underset{\dot{}}{\le }x\right)$$
16	14 15	imbi12d	$$⊢z=x\to \left(\left(\forall y\in Sy\underset{\dot{}}{\le }z\to w\underset{\dot{}}{\le }z\right)\leftrightarrow \left(\forall y\in Sy\underset{\dot{}}{\le }x\to w\underset{\dot{}}{\le }x\right)\right)$$
17		simprrr	$$⊢\left(\left(\left(K\in \mathrm{Poset}\wedge S\subseteq B\right)\wedge \left(x\in B\wedge w\in B\right)\right)\wedge \left(\left(\forall y\in Sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\wedge \left(\forall y\in Sy\underset{\dot{}}{\le }w\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to w\underset{\dot{}}{\le }z\right)\right)\right)\right)\to \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to w\underset{\dot{}}{\le }z\right)$$
18		simplrl	$$⊢\left(\left(\left(K\in \mathrm{Poset}\wedge S\subseteq B\right)\wedge \left(x\in B\wedge w\in B\right)\right)\wedge \left(\left(\forall y\in Sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\wedge \left(\forall y\in Sy\underset{\dot{}}{\le }w\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to w\underset{\dot{}}{\le }z\right)\right)\right)\right)\to x\in B$$
19	16 17 18	rspcdva	$$⊢\left(\left(\left(K\in \mathrm{Poset}\wedge S\subseteq B\right)\wedge \left(x\in B\wedge w\in B\right)\right)\wedge \left(\left(\forall y\in Sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\wedge \left(\forall y\in Sy\underset{\dot{}}{\le }w\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to w\underset{\dot{}}{\le }z\right)\right)\right)\right)\to \left(\forall y\in Sy\underset{\dot{}}{\le }x\to w\underset{\dot{}}{\le }x\right)$$
20	12 19	mpd	$$⊢\left(\left(\left(K\in \mathrm{Poset}\wedge S\subseteq B\right)\wedge \left(x\in B\wedge w\in B\right)\right)\wedge \left(\left(\forall y\in Sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\wedge \left(\forall y\in Sy\underset{\dot{}}{\le }w\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to w\underset{\dot{}}{\le }z\right)\right)\right)\right)\to w\underset{\dot{}}{\le }x$$
21	2 1	posasymb	$$⊢\left(K\in \mathrm{Poset}\wedge x\in B\wedge w\in B\right)\to \left(\left(x\underset{\dot{}}{\le }w\wedge w\underset{\dot{}}{\le }x\right)\leftrightarrow x=w\right)$$
22	21	3expb	$$⊢\left(K\in \mathrm{Poset}\wedge \left(x\in B\wedge w\in B\right)\right)\to \left(\left(x\underset{\dot{}}{\le }w\wedge w\underset{\dot{}}{\le }x\right)\leftrightarrow x=w\right)$$
23	22	ad4ant13	$$⊢\left(\left(\left(K\in \mathrm{Poset}\wedge S\subseteq B\right)\wedge \left(x\in B\wedge w\in B\right)\right)\wedge \left(\left(\forall y\in Sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\wedge \left(\forall y\in Sy\underset{\dot{}}{\le }w\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to w\underset{\dot{}}{\le }z\right)\right)\right)\right)\to \left(\left(x\underset{\dot{}}{\le }w\wedge w\underset{\dot{}}{\le }x\right)\leftrightarrow x=w\right)$$
24	11 20 23	mpbi2and	$$⊢\left(\left(\left(K\in \mathrm{Poset}\wedge S\subseteq B\right)\wedge \left(x\in B\wedge w\in B\right)\right)\wedge \left(\left(\forall y\in Sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\wedge \left(\forall y\in Sy\underset{\dot{}}{\le }w\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to w\underset{\dot{}}{\le }z\right)\right)\right)\right)\to x=w$$
25	24	ex	$$⊢\left(\left(K\in \mathrm{Poset}\wedge S\subseteq B\right)\wedge \left(x\in B\wedge w\in B\right)\right)\to \left(\left(\left(\forall y\in Sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\wedge \left(\forall y\in Sy\underset{\dot{}}{\le }w\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to w\underset{\dot{}}{\le }z\right)\right)\right)\to x=w\right)$$
26	25	ralrimivva	$$⊢\left(K\in \mathrm{Poset}\wedge S\subseteq B\right)\to \forall x\in B\forall w\in B\left(\left(\left(\forall y\in Sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\wedge \left(\forall y\in Sy\underset{\dot{}}{\le }w\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to w\underset{\dot{}}{\le }z\right)\right)\right)\to x=w\right)$$
27		breq2	$$⊢x=w\to \left(y\underset{\dot{}}{\le }x\leftrightarrow y\underset{\dot{}}{\le }w\right)$$
28	27	ralbidv	$$⊢x=w\to \left(\forall y\in Sy\underset{\dot{}}{\le }x\leftrightarrow \forall y\in Sy\underset{\dot{}}{\le }w\right)$$
29		breq1	$$⊢x=w\to \left(x\underset{\dot{}}{\le }z\leftrightarrow w\underset{\dot{}}{\le }z\right)$$
30	29	imbi2d	$$⊢x=w\to \left(\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\leftrightarrow \left(\forall y\in Sy\underset{\dot{}}{\le }z\to w\underset{\dot{}}{\le }z\right)\right)$$
31	30	ralbidv	$$⊢x=w\to \left(\forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\leftrightarrow \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to w\underset{\dot{}}{\le }z\right)\right)$$
32	28 31	anbi12d	$$⊢x=w\to \left(\left(\forall y\in Sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\leftrightarrow \left(\forall y\in Sy\underset{\dot{}}{\le }w\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to w\underset{\dot{}}{\le }z\right)\right)\right)$$
33	32	rmo4	$$⊢{\exists }^{*}x\in B\left(\forall y\in Sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\leftrightarrow \forall x\in B\forall w\in B\left(\left(\left(\forall y\in Sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\wedge \left(\forall y\in Sy\underset{\dot{}}{\le }w\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to w\underset{\dot{}}{\le }z\right)\right)\right)\to x=w\right)$$
34	26 33	sylibr	$$⊢\left(K\in \mathrm{Poset}\wedge S\subseteq B\right)\to {\exists }^{*}x\in B\left(\forall y\in Sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)$$