Theorem poslubdg

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

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

Proof

Step	Hyp	Ref	Expression
1		poslubdg.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		poslubdg.b	$$⊢\phi \to B={\mathrm{Base}}_K$$
3		poslubdg.u	$$⊢\phi \to U=\mathrm{lub}\left(K\right)$$
4		poslubdg.k	$$⊢\phi \to K\in \mathrm{Poset}$$
5		poslubdg.s	$$⊢\phi \to S\subseteq B$$
6		poslubdg.t	$$⊢\phi \to T\in B$$
7		poslubdg.ub	$$⊢\left(\phi \wedge x\in S\right)\to x\underset{\dot{}}{\le }T$$
8		poslubdg.le	$$⊢\left(\phi \wedge y\in B\wedge \forall x\in Sx\underset{\dot{}}{\le }y\right)\to T\underset{\dot{}}{\le }y$$
9	3	fveq1d	$$⊢\phi \to U\left(S\right)=\mathrm{lub}\left(K\right)\left(S\right)$$
10		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
11		eqid	$$⊢\mathrm{lub}\left(K\right)=\mathrm{lub}\left(K\right)$$
12	5 2	sseqtrd	$$⊢\phi \to S\subseteq {\mathrm{Base}}_K$$
13	6 2	eleqtrd	$$⊢\phi \to T\in {\mathrm{Base}}_K$$
14	2	eleq2d	$$⊢\phi \to \left(y\in B\leftrightarrow y\in {\mathrm{Base}}_K\right)$$
15	14	biimpar	$$⊢\left(\phi \wedge y\in {\mathrm{Base}}_K\right)\to y\in B$$
16	15	3adant3	$$⊢\left(\phi \wedge y\in {\mathrm{Base}}_K\wedge \forall x\in Sx\underset{\dot{}}{\le }y\right)\to y\in B$$
17	16 8	syld3an2	$$⊢\left(\phi \wedge y\in {\mathrm{Base}}_K\wedge \forall x\in Sx\underset{\dot{}}{\le }y\right)\to T\underset{\dot{}}{\le }y$$
18	1 10 11 4 12 13 7 17	poslubd	$$⊢\phi \to \mathrm{lub}\left(K\right)\left(S\right)=T$$
19	9 18	eqtrd	$$⊢\phi \to U\left(S\right)=T$$