Theorem isglbd

Description: Properties that determine the greatest lower bound of a complete lattice. (Contributed by Mario Carneiro, 19-Mar-2014)

	Ref	Expression
Hypotheses	isglbd.b	$$⊢B={\mathrm{Base}}_K$$
	isglbd.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	isglbd.g	$$⊢G=\mathrm{glb}\left(K\right)$$
	isglbd.1	$$⊢\left(\phi \wedge y\in S\right)\to H\underset{\dot{}}{\le }y$$
	isglbd.2	$$⊢\left(\phi \wedge x\in B\wedge \forall y\in Sx\underset{\dot{}}{\le }y\right)\to x\underset{\dot{}}{\le }H$$
	isglbd.3	$$⊢\phi \to K\in \mathrm{CLat}$$
	isglbd.4	$$⊢\phi \to S\subseteq B$$
	isglbd.5	$$⊢\phi \to H\in B$$
Assertion	isglbd	$$⊢\phi \to G\left(S\right)=H$$

Proof

Step	Hyp	Ref	Expression
1		isglbd.b	$$⊢B={\mathrm{Base}}_K$$
2		isglbd.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		isglbd.g	$$⊢G=\mathrm{glb}\left(K\right)$$
4		isglbd.1	$$⊢\left(\phi \wedge y\in S\right)\to H\underset{\dot{}}{\le }y$$
5		isglbd.2	$$⊢\left(\phi \wedge x\in B\wedge \forall y\in Sx\underset{\dot{}}{\le }y\right)\to x\underset{\dot{}}{\le }H$$
6		isglbd.3	$$⊢\phi \to K\in \mathrm{CLat}$$
7		isglbd.4	$$⊢\phi \to S\subseteq B$$
8		isglbd.5	$$⊢\phi \to H\in B$$
9		biid	$$⊢\left(\forall y\in Sh\underset{\dot{}}{\le }y\wedge \forall x\in B\left(\forall y\in Sx\underset{\dot{}}{\le }y\to x\underset{\dot{}}{\le }h\right)\right)\leftrightarrow \left(\forall y\in Sh\underset{\dot{}}{\le }y\wedge \forall x\in B\left(\forall y\in Sx\underset{\dot{}}{\le }y\to x\underset{\dot{}}{\le }h\right)\right)$$
10	1 2 3 9 6 7	glbval	$$⊢\phi \to G\left(S\right)=\left(\iota h\in B|\left(\forall y\in Sh\underset{\dot{}}{\le }y\wedge \forall x\in B\left(\forall y\in Sx\underset{\dot{}}{\le }y\to x\underset{\dot{}}{\le }h\right)\right)\right)$$
11	4	ralrimiva	$$⊢\phi \to \forall y\in SH\underset{\dot{}}{\le }y$$
12	5	3exp	$$⊢\phi \to \left(x\in B\to \left(\forall y\in Sx\underset{\dot{}}{\le }y\to x\underset{\dot{}}{\le }H\right)\right)$$
13	12	ralrimiv	$$⊢\phi \to \forall x\in B\left(\forall y\in Sx\underset{\dot{}}{\le }y\to x\underset{\dot{}}{\le }H\right)$$
14	1 3	clatglbcl2	$$⊢\left(K\in \mathrm{CLat}\wedge S\subseteq B\right)\to S\in \mathrm{dom}G$$
15	6 7 14	syl2anc	$$⊢\phi \to S\in \mathrm{dom}G$$
16	1 2 3 9 6 15	glbeu	$$⊢\phi \to \exists !h\in B\left(\forall y\in Sh\underset{\dot{}}{\le }y\wedge \forall x\in B\left(\forall y\in Sx\underset{\dot{}}{\le }y\to x\underset{\dot{}}{\le }h\right)\right)$$
17		breq1	$$⊢h=H\to \left(h\underset{\dot{}}{\le }y\leftrightarrow H\underset{\dot{}}{\le }y\right)$$
18	17	ralbidv	$$⊢h=H\to \left(\forall y\in Sh\underset{\dot{}}{\le }y\leftrightarrow \forall y\in SH\underset{\dot{}}{\le }y\right)$$
19		breq2	$$⊢h=H\to \left(x\underset{\dot{}}{\le }h\leftrightarrow x\underset{\dot{}}{\le }H\right)$$
20	19	imbi2d	$$⊢h=H\to \left(\left(\forall y\in Sx\underset{\dot{}}{\le }y\to x\underset{\dot{}}{\le }h\right)\leftrightarrow \left(\forall y\in Sx\underset{\dot{}}{\le }y\to x\underset{\dot{}}{\le }H\right)\right)$$
21	20	ralbidv	$$⊢h=H\to \left(\forall x\in B\left(\forall y\in Sx\underset{\dot{}}{\le }y\to x\underset{\dot{}}{\le }h\right)\leftrightarrow \forall x\in B\left(\forall y\in Sx\underset{\dot{}}{\le }y\to x\underset{\dot{}}{\le }H\right)\right)$$
22	18 21	anbi12d	$$⊢h=H\to \left(\left(\forall y\in Sh\underset{\dot{}}{\le }y\wedge \forall x\in B\left(\forall y\in Sx\underset{\dot{}}{\le }y\to x\underset{\dot{}}{\le }h\right)\right)\leftrightarrow \left(\forall y\in SH\underset{\dot{}}{\le }y\wedge \forall x\in B\left(\forall y\in Sx\underset{\dot{}}{\le }y\to x\underset{\dot{}}{\le }H\right)\right)\right)$$
23	22	riota2	$$⊢\left(H\in B\wedge \exists !h\in B\left(\forall y\in Sh\underset{\dot{}}{\le }y\wedge \forall x\in B\left(\forall y\in Sx\underset{\dot{}}{\le }y\to x\underset{\dot{}}{\le }h\right)\right)\right)\to \left(\left(\forall y\in SH\underset{\dot{}}{\le }y\wedge \forall x\in B\left(\forall y\in Sx\underset{\dot{}}{\le }y\to x\underset{\dot{}}{\le }H\right)\right)\leftrightarrow \left(\iota h\in B|\left(\forall y\in Sh\underset{\dot{}}{\le }y\wedge \forall x\in B\left(\forall y\in Sx\underset{\dot{}}{\le }y\to x\underset{\dot{}}{\le }h\right)\right)\right)=H\right)$$
24	8 16 23	syl2anc	$$⊢\phi \to \left(\left(\forall y\in SH\underset{\dot{}}{\le }y\wedge \forall x\in B\left(\forall y\in Sx\underset{\dot{}}{\le }y\to x\underset{\dot{}}{\le }H\right)\right)\leftrightarrow \left(\iota h\in B|\left(\forall y\in Sh\underset{\dot{}}{\le }y\wedge \forall x\in B\left(\forall y\in Sx\underset{\dot{}}{\le }y\to x\underset{\dot{}}{\le }h\right)\right)\right)=H\right)$$
25	11 13 24	mpbi2and	$$⊢\phi \to \left(\iota h\in B|\left(\forall y\in Sh\underset{\dot{}}{\le }y\wedge \forall x\in B\left(\forall y\in Sx\underset{\dot{}}{\le }y\to x\underset{\dot{}}{\le }h\right)\right)\right)=H$$
26	10 25	eqtrd	$$⊢\phi \to G\left(S\right)=H$$