Theorem poslubd

Description: Properties which determine the least upper bound in a poset. (Contributed by Stefan O'Rear, 31-Jan-2015)

	Ref	Expression
Hypotheses	poslubd.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	poslubd.b	$$⊢B={\mathrm{Base}}_K$$
	poslubd.u	$$⊢U=\mathrm{lub}\left(K\right)$$
	poslubd.k	$$⊢\phi \to K\in \mathrm{Poset}$$
	poslubd.s	$$⊢\phi \to S\subseteq B$$
	poslubd.t	$$⊢\phi \to T\in B$$
	poslubd.ub	$$⊢\left(\phi \wedge x\in S\right)\to x\underset{\dot{}}{\le }T$$
	poslubd.le	$$⊢\left(\phi \wedge y\in B\wedge \forall x\in Sx\underset{\dot{}}{\le }y\right)\to T\underset{\dot{}}{\le }y$$
Assertion	poslubd	$$⊢\phi \to U\left(S\right)=T$$

Proof

Step	Hyp	Ref	Expression
1		poslubd.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		poslubd.b	$$⊢B={\mathrm{Base}}_K$$
3		poslubd.u	$$⊢U=\mathrm{lub}\left(K\right)$$
4		poslubd.k	$$⊢\phi \to K\in \mathrm{Poset}$$
5		poslubd.s	$$⊢\phi \to S\subseteq B$$
6		poslubd.t	$$⊢\phi \to T\in B$$
7		poslubd.ub	$$⊢\left(\phi \wedge x\in S\right)\to x\underset{\dot{}}{\le }T$$
8		poslubd.le	$$⊢\left(\phi \wedge y\in B\wedge \forall x\in Sx\underset{\dot{}}{\le }y\right)\to T\underset{\dot{}}{\le }y$$
9		biid	$$⊢\left(\forall x\in Sx\underset{\dot{}}{\le }z\wedge \forall y\in B\left(\forall x\in Sx\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }y\right)\right)\leftrightarrow \left(\forall x\in Sx\underset{\dot{}}{\le }z\wedge \forall y\in B\left(\forall x\in Sx\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }y\right)\right)$$
10	2 1 3 9 4 5	lubval	$$⊢\phi \to U\left(S\right)=\left(\iota z\in B|\left(\forall x\in Sx\underset{\dot{}}{\le }z\wedge \forall y\in B\left(\forall x\in Sx\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }y\right)\right)\right)$$
11	7	ralrimiva	$$⊢\phi \to \forall x\in Sx\underset{\dot{}}{\le }T$$
12	8	3expia	$$⊢\left(\phi \wedge y\in B\right)\to \left(\forall x\in Sx\underset{\dot{}}{\le }y\to T\underset{\dot{}}{\le }y\right)$$
13	12	ralrimiva	$$⊢\phi \to \forall y\in B\left(\forall x\in Sx\underset{\dot{}}{\le }y\to T\underset{\dot{}}{\le }y\right)$$
14	11 13	jca	$$⊢\phi \to \left(\forall x\in Sx\underset{\dot{}}{\le }T\wedge \forall y\in B\left(\forall x\in Sx\underset{\dot{}}{\le }y\to T\underset{\dot{}}{\le }y\right)\right)$$
15		breq2	$$⊢z=T\to \left(x\underset{\dot{}}{\le }z\leftrightarrow x\underset{\dot{}}{\le }T\right)$$
16	15	ralbidv	$$⊢z=T\to \left(\forall x\in Sx\underset{\dot{}}{\le }z\leftrightarrow \forall x\in Sx\underset{\dot{}}{\le }T\right)$$
17		breq1	$$⊢z=T\to \left(z\underset{\dot{}}{\le }y\leftrightarrow T\underset{\dot{}}{\le }y\right)$$
18	17	imbi2d	$$⊢z=T\to \left(\left(\forall x\in Sx\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }y\right)\leftrightarrow \left(\forall x\in Sx\underset{\dot{}}{\le }y\to T\underset{\dot{}}{\le }y\right)\right)$$
19	18	ralbidv	$$⊢z=T\to \left(\forall y\in B\left(\forall x\in Sx\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }y\right)\leftrightarrow \forall y\in B\left(\forall x\in Sx\underset{\dot{}}{\le }y\to T\underset{\dot{}}{\le }y\right)\right)$$
20	16 19	anbi12d	$$⊢z=T\to \left(\left(\forall x\in Sx\underset{\dot{}}{\le }z\wedge \forall y\in B\left(\forall x\in Sx\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }y\right)\right)\leftrightarrow \left(\forall x\in Sx\underset{\dot{}}{\le }T\wedge \forall y\in B\left(\forall x\in Sx\underset{\dot{}}{\le }y\to T\underset{\dot{}}{\le }y\right)\right)\right)$$
21	20	rspcev	$$⊢\left(T\in B\wedge \left(\forall x\in Sx\underset{\dot{}}{\le }T\wedge \forall y\in B\left(\forall x\in Sx\underset{\dot{}}{\le }y\to T\underset{\dot{}}{\le }y\right)\right)\right)\to \exists z\in B\left(\forall x\in Sx\underset{\dot{}}{\le }z\wedge \forall y\in B\left(\forall x\in Sx\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }y\right)\right)$$
22	6 14 21	syl2anc	$$⊢\phi \to \exists z\in B\left(\forall x\in Sx\underset{\dot{}}{\le }z\wedge \forall y\in B\left(\forall x\in Sx\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }y\right)\right)$$
23	1 2	poslubmo	$$⊢\left(K\in \mathrm{Poset}\wedge S\subseteq B\right)\to {\exists }^{*}z\in B\left(\forall x\in Sx\underset{\dot{}}{\le }z\wedge \forall y\in B\left(\forall x\in Sx\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }y\right)\right)$$
24	4 5 23	syl2anc	$$⊢\phi \to {\exists }^{*}z\in B\left(\forall x\in Sx\underset{\dot{}}{\le }z\wedge \forall y\in B\left(\forall x\in Sx\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }y\right)\right)$$
25		reu5	$$⊢\exists !z\in B\left(\forall x\in Sx\underset{\dot{}}{\le }z\wedge \forall y\in B\left(\forall x\in Sx\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }y\right)\right)\leftrightarrow \left(\exists z\in B\left(\forall x\in Sx\underset{\dot{}}{\le }z\wedge \forall y\in B\left(\forall x\in Sx\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }y\right)\right)\wedge {\exists }^{*}z\in B\left(\forall x\in Sx\underset{\dot{}}{\le }z\wedge \forall y\in B\left(\forall x\in Sx\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }y\right)\right)\right)$$
26	22 24 25	sylanbrc	$$⊢\phi \to \exists !z\in B\left(\forall x\in Sx\underset{\dot{}}{\le }z\wedge \forall y\in B\left(\forall x\in Sx\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }y\right)\right)$$
27	20	riota2	$$⊢\left(T\in B\wedge \exists !z\in B\left(\forall x\in Sx\underset{\dot{}}{\le }z\wedge \forall y\in B\left(\forall x\in Sx\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }y\right)\right)\right)\to \left(\left(\forall x\in Sx\underset{\dot{}}{\le }T\wedge \forall y\in B\left(\forall x\in Sx\underset{\dot{}}{\le }y\to T\underset{\dot{}}{\le }y\right)\right)\leftrightarrow \left(\iota z\in B|\left(\forall x\in Sx\underset{\dot{}}{\le }z\wedge \forall y\in B\left(\forall x\in Sx\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }y\right)\right)\right)=T\right)$$
28	6 26 27	syl2anc	$$⊢\phi \to \left(\left(\forall x\in Sx\underset{\dot{}}{\le }T\wedge \forall y\in B\left(\forall x\in Sx\underset{\dot{}}{\le }y\to T\underset{\dot{}}{\le }y\right)\right)\leftrightarrow \left(\iota z\in B|\left(\forall x\in Sx\underset{\dot{}}{\le }z\wedge \forall y\in B\left(\forall x\in Sx\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }y\right)\right)\right)=T\right)$$
29	14 28	mpbid	$$⊢\phi \to \left(\iota z\in B|\left(\forall x\in Sx\underset{\dot{}}{\le }z\wedge \forall y\in B\left(\forall x\in Sx\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }y\right)\right)\right)=T$$
30	10 29	eqtrd	$$⊢\phi \to U\left(S\right)=T$$